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  4283  frirrg  4442  ordtri2or2exmid  4664  ontri2orexmidim  4665  riotass  5993  elovimad  6054  tfrcldm  6520  nntr2  6662  eroveu  6786  eroprf  6788  ixpssmapg  6888  findcard2d  7066  findcard2sd  7067  fimax2gtrilemstep  7076  elssdc  7080  eqsndc  7081  undifdc  7102  fisseneq  7112  fidcenumlemrks  7136  fidcenumlemr  7138  fiuni  7161  suplub2ti  7184  ctssdclemn0  7293  acfun  7405  ccfunen  7466  nnppipi  7546  archnqq  7620  prarloclemlt  7696  suplocexprlemrl  7920  suplocexprlemmu  7921  suplocexprlemdisj  7923  suplocexprlemloc  7924  suplocexprlemex  7925  suplocexprlemub  7926  suplocexprlemlub  7927  suplocsrlemb  8009  suplocsrlempr  8010  suplocsrlem  8011  axpre-suploclemres  8104  suprubex  9114  suprzclex  9561  infregelbex  9810  fzssp1  10280  elfzoelz  10360  fzofzp1  10450  fzostep1  10460  zssinfcl  10469  suprzubdc  10473  zsupssdc  10475  suprzcl2dc  10476  frecuzrdgg  10655  frecuzrdgdomlem  10656  frecuzrdgsuctlem  10662  ser3mono  10726  seqf1oglem2a  10757  seqf1oglem2  10759  bcm1k  10999  fimaxq  11067  leisorel  11077  zfz1isolemiso  11079  seq3coll  11082  fun2dmnop0  11087  swrdclg  11203  fimaxre2  11759  summodclem2a  11913  fsum3cvg3  11928  fsumcl2lem  11930  fsum0diaglem  11972  fsumiun  12009  prodmodclem2a  12108  fprodcl2lem  12137  fprodap0  12153  fprodrec  12161  fprodap0f  12168  fprodle  12172  bitsfzolem  12486  bitsfzo  12487  uzwodc  12579  4sqlemffi  12940  ennnfonelemhom  13007  exmidunben  13018  ctiunctlemfo  13031  nninfdclemcl  13040  nninfdclemp1  13042  nninfdclemlt  13043  nninfdclemf1  13044  unbendc  13046  strsetsid  13086  strslssd  13100  gsumpropd2  13447  gsumress  13449  resmhm  13541  mhmima  13545  grpidssd  13630  grpinvssd  13631  mulgnnsubcl  13692  mulgnn0subcl  13693  mulgsubcl  13694  mulgpropdg  13722  submmulg  13724  subg0  13738  subgsubcl  13743  subgsub  13744  subgmulg  13746  issubg4m  13751  nsgconj  13764  ssnmz  13769  ghmnsgima  13826  subgabl  13890  rdivmuldivd  14129  rhmunitinv  14163  subrguss  14221  subrginv  14222  subrgdv  14223  lsselg  14346  islss3  14364  lspsnel3  14390  lsspropdg  14416  rnglidlmcl  14465  znf1o  14636  topssnei  14857  cnprcl2k  14901  cnss1  14921  cnptopresti  14933  cnptoprest  14934  lmres  14943  txopn  14960  txcnp  14966  xmetres2  15074  blin2  15127  blopn  15185  xmettxlem  15204  xmettx  15205  elcncf2  15269  cncfmet  15287  cncfmptc  15291  cncfmptid  15292  negcncf  15300  mulcncflem  15302  cnrehmeocntop  15305  dedekindeulemuub  15312  dedekindeulemlu  15316  suplociccreex  15319  suplociccex  15320  dedekindicclemuub  15321  dedekindicclemlu  15325  dedekindicclemeu  15326  dedekindicclemicc  15327  ivthinclemlopn  15331  ivthinclemuopn  15333  ivthdec  15339  limcimolemlt  15359  cnplimcim  15362  cnplimclemle  15363  cnplimclemr  15364  cnlimci  15368  limccnpcntop  15370  limccnp2lem  15371  limccnp2cntop  15372  dvlemap  15375  dvfgg  15383  dvidsslem  15388  dvconstss  15393  dvcnp2cntop  15394  dvaddxxbr  15396  dvmulxxbr  15397  dvcoapbr  15402  dvcjbr  15403  plyf  15432  plycolemc  15453  dvply2g  15461  reeff1olem  15466  lgsquadlem3  15779  upgrex  15924  wlkvtxiedg  16117  wlkvtxiedgg  16118  sssneq  16481