Theorem sseldd 3225

Description: Membership inference from subclass relationship. (Contributed by NM, 14-Dec-2004.)

Hypotheses

Ref	Expression
sseld.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
sseldd.2	⊢ (𝜑 → 𝐶 ∈ 𝐴)

Assertion

Ref	Expression
sseldd	⊢ (𝜑 → 𝐶 ∈ 𝐵)

Proof of Theorem sseldd

Step	Hyp	Ref	Expression
1		sseldd.2	. 2 ⊢ (𝜑 → 𝐶 ∈ 𝐴)
2		sseld.1	. . 3 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
3	2	sseld 3223	. 2 ⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
4	1, 3	mpd 13	1 ⊢ (𝜑 → 𝐶 ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2200   ⊆ wss 3197

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  disjiun  4078  exmid01  4282  frirrg  4441  ordtri2or2exmid  4663  ontri2orexmidim  4664  riotass  5990  elovimad  6051  tfrcldm  6515  nntr2  6657  eroveu  6781  eroprf  6783  ixpssmapg  6883  findcard2d  7061  findcard2sd  7062  fimax2gtrilemstep  7070  undifdc  7094  fisseneq  7104  fidcenumlemrks  7128  fidcenumlemr  7130  fiuni  7153  suplub2ti  7176  ctssdclemn0  7285  acfun  7397  ccfunen  7458  nnppipi  7538  archnqq  7612  prarloclemlt  7688  suplocexprlemrl  7912  suplocexprlemmu  7913  suplocexprlemdisj  7915  suplocexprlemloc  7916  suplocexprlemex  7917  suplocexprlemub  7918  suplocexprlemlub  7919  suplocsrlemb  8001  suplocsrlempr  8002  suplocsrlem  8003  axpre-suploclemres  8096  suprubex  9106  suprzclex  9553  infregelbex  9801  fzssp1  10271  elfzoelz  10351  fzofzp1  10441  fzostep1  10451  zssinfcl  10460  suprzubdc  10464  zsupssdc  10466  suprzcl2dc  10467  frecuzrdgg  10646  frecuzrdgdomlem  10647  frecuzrdgsuctlem  10653  ser3mono  10717  seqf1oglem2a  10748  seqf1oglem2  10750  bcm1k  10990  fimaxq  11057  leisorel  11067  zfz1isolemiso  11069  seq3coll  11072  fun2dmnop0  11077  swrdclg  11190  fimaxre2  11746  summodclem2a  11900  fsum3cvg3  11915  fsumcl2lem  11917  fsum0diaglem  11959  fsumiun  11996  prodmodclem2a  12095  fprodcl2lem  12124  fprodap0  12140  fprodrec  12148  fprodap0f  12155  fprodle  12159  bitsfzolem  12473  bitsfzo  12474  uzwodc  12566  4sqlemffi  12927  ennnfonelemhom  12994  exmidunben  13005  ctiunctlemfo  13018  nninfdclemcl  13027  nninfdclemp1  13029  nninfdclemlt  13030  nninfdclemf1  13031  unbendc  13033  strsetsid  13073  strslssd  13087  gsumpropd2  13434  gsumress  13436  resmhm  13528  mhmima  13532  grpidssd  13617  grpinvssd  13618  mulgnnsubcl  13679  mulgnn0subcl  13680  mulgsubcl  13681  mulgpropdg  13709  submmulg  13711  subg0  13725  subgsubcl  13730  subgsub  13731  subgmulg  13733  issubg4m  13738  nsgconj  13751  ssnmz  13756  ghmnsgima  13813  subgabl  13877  rdivmuldivd  14116  rhmunitinv  14150  subrguss  14208  subrginv  14209  subrgdv  14210  lsselg  14333  islss3  14351  lspsnel3  14377  lsspropdg  14403  rnglidlmcl  14452  znf1o  14623  topssnei  14844  cnprcl2k  14888  cnss1  14908  cnptopresti  14920  cnptoprest  14921  lmres  14930  txopn  14947  txcnp  14953  xmetres2  15061  blin2  15114  blopn  15172  xmettxlem  15191  xmettx  15192  elcncf2  15256  cncfmet  15274  cncfmptc  15278  cncfmptid  15279  negcncf  15287  mulcncflem  15289  cnrehmeocntop  15292  dedekindeulemuub  15299  dedekindeulemlu  15303  suplociccreex  15306  suplociccex  15307  dedekindicclemuub  15308  dedekindicclemlu  15312  dedekindicclemeu  15313  dedekindicclemicc  15314  ivthinclemlopn  15318  ivthinclemuopn  15320  ivthdec  15326  limcimolemlt  15346  cnplimcim  15349  cnplimclemle  15350  cnplimclemr  15351  cnlimci  15355  limccnpcntop  15357  limccnp2lem  15358  limccnp2cntop  15359  dvlemap  15362  dvfgg  15370  dvidsslem  15375  dvconstss  15380  dvcnp2cntop  15381  dvaddxxbr  15383  dvmulxxbr  15384  dvcoapbr  15389  dvcjbr  15390  plyf  15419  plycolemc  15440  dvply2g  15448  reeff1olem  15453  lgsquadlem3  15766  upgrex  15911  wlkvtxiedg  16066  wlkvtxiedgg  16067  sssneq  16397