Theorem sseli 2068

Description: Membership inference from subclass relationship.

Hypothesis

Ref	Expression
sseli.1	⊢ A ⊆ B

Assertion

Ref	Expression
sseli	⊢ (C ∈ A → C ∈ B)

Proof of Theorem sseli

Step	Hyp	Ref	Expression
1		sseli.1	. 2 ⊢ A ⊆ B
2		ssel 2066	. 2 ⊢ (A ⊆ B → (C ∈ A → C ∈ B))
3	1, 2	ax-mp 7	1 ⊢ (C ∈ A → C ∈ B)

Syntax hints:   → wi 3   ∈ wcel 960   ⊆ wss 2050

This theorem is referenced by:  sselii 2069  elun1 2200  elun2 2201  onfr 2992  nnont 3144  finds 3162  finds2 3164  brelg 3228  asymref 3445  asymref2 3446  2elresin 3604  fvopab4ndm 3790  fvimacnvi 3810  tz7.44-3 3936  eloprabi 4124  zfregs 4657  tz9.12lem3 4671  cplem1 4730  hta 4738  kmlem1 4775  zorn2lem3 4800  zorn2lem4 4801  zorn2lem5 4802  brdom5 4812  brdom4 4813  alephfplem3 4909  alephfp 4911  pinn 5018  recnt 5325  rexrt 5511  nnret 5931  nncnt 5932  nnind 5939  lbcl 6048  nnnn0t 6108  nn0ret 6110  nn0cnt 6111  nnzt 6155  nn0zt 6156  dfuz 6204  uzwo4OLD 6212  nnqt 6267  qcnt 6268  rpret 6285  om2uzlt 6299  om2uzlt2 6300  om2uzf1o 6302  uzssz 6431  expcllem 6576  cau3i 6914  cau5i 6917  cvg3 6923  clm3 7079  clm4 7080  clm4f 7082  climconst 7094  serzf0 7169  ser1f0 7170  ivthlem5 7285  dsupivthlem 7291  efsep 7396  unbenlem 7505  tgval2t 7616  cncnplem4 7774  caussi 7951  bcthlem14 8009  issubgi 8118  ghsubgi 8134  vcoprnelem 8193  vcex 8195  nvvcop 8209  nvvop 8224  phnv 8469  minveclem4 8544  minveclem5 8545  minveclem9 8549  minveclem10 8550  minveclem14 8554  minveclem16 8556  minveclem17 8557  minveclem28 8568  minveclem30 8570  minveclem31 8571  minveclem38 8578  minveceu 8579  pilem1 8666  pilem2 8667  efghgrpilem 8714  efifolem1 8717  relogeft 8758  relogeftb 8760  explogt 8767  shel 9077  chsh 9091  chel 9097  occl 9176  choc1 9286  shintcl 9288  chintcl 9290  shslej 9333  osumlem2 9574  osumlem4 9576  pjocin 9638  pjin 9639  mayete3 9668  dmadjopt 9815  nlelsh 9988  cnlnadjeu 10005  cnlnssadj 10008  bdopadjt 10010  hmopidmch 10074  hmopidmpj 10075  pjima 10099  atelch 10266  nnssi2 10414  nnssi3 10415  inposet 10477  cdrci 10480  dmhmpha 10520  rnhmpha 10521  fgsb 10555  fgsb2 10560  iintlem2 10604

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-in 2054  df-ss 2056

Copyright terms: Public domain