Theorem sseldd 3228

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 3226	. 2 ⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
4	1, 3	mpd 13	1 ⊢ (𝜑 → 𝐶 ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2202   ⊆ wss 3200

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  disjiun  4083  exmid01  4288  frirrg  4447  ordtri2or2exmid  4669  ontri2orexmidim  4670  riotass  6001  elovimad  6062  tfrcldm  6529  nntr2  6671  eroveu  6795  eroprf  6797  ixpssmapg  6897  findcard2d  7080  findcard2sd  7081  fimax2gtrilemstep  7090  elssdc  7094  eqsndc  7095  undifdc  7116  fisseneq  7127  fidcenumlemrks  7152  fidcenumlemr  7154  fiuni  7177  suplub2ti  7200  ctssdclemn0  7309  acfun  7422  ccfunen  7483  nnppipi  7563  archnqq  7637  prarloclemlt  7713  suplocexprlemrl  7937  suplocexprlemmu  7938  suplocexprlemdisj  7940  suplocexprlemloc  7941  suplocexprlemex  7942  suplocexprlemub  7943  suplocexprlemlub  7944  suplocsrlemb  8026  suplocsrlempr  8027  suplocsrlem  8028  axpre-suploclemres  8121  suprubex  9131  suprzclex  9578  infregelbex  9832  fzssp1  10302  elfzoelz  10382  fzofzp1  10473  fzostep1  10484  zssinfcl  10493  suprzubdc  10497  zsupssdc  10499  suprzcl2dc  10500  frecuzrdgg  10679  frecuzrdgdomlem  10680  frecuzrdgsuctlem  10686  ser3mono  10750  seqf1oglem2a  10781  seqf1oglem2  10783  bcm1k  11023  fimaxq  11092  leisorel  11102  zfz1isolemiso  11104  seq3coll  11107  fun2dmnop0  11112  swrdclg  11232  fimaxre2  11789  summodclem2a  11944  fsum3cvg3  11959  fsumcl2lem  11961  fsum0diaglem  12003  fsumiun  12040  prodmodclem2a  12139  fprodcl2lem  12168  fprodap0  12184  fprodrec  12192  fprodap0f  12199  fprodle  12203  bitsfzolem  12517  bitsfzo  12518  uzwodc  12610  4sqlemffi  12971  ennnfonelemhom  13038  exmidunben  13049  ctiunctlemfo  13062  nninfdclemcl  13071  nninfdclemp1  13073  nninfdclemlt  13074  nninfdclemf1  13075  unbendc  13077  strsetsid  13117  strslssd  13131  gsumpropd2  13478  gsumress  13480  resmhm  13572  mhmima  13576  grpidssd  13661  grpinvssd  13662  mulgnnsubcl  13723  mulgnn0subcl  13724  mulgsubcl  13725  mulgpropdg  13753  submmulg  13755  subg0  13769  subgsubcl  13774  subgsub  13775  subgmulg  13777  issubg4m  13782  nsgconj  13795  ssnmz  13800  ghmnsgima  13857  subgabl  13921  rdivmuldivd  14161  rhmunitinv  14195  subrguss  14253  subrginv  14254  subrgdv  14255  lsselg  14378  islss3  14396  lspsnel3  14422  lsspropdg  14448  rnglidlmcl  14497  znf1o  14668  topssnei  14889  cnprcl2k  14933  cnss1  14953  cnptopresti  14965  cnptoprest  14966  lmres  14975  txopn  14992  txcnp  14998  xmetres2  15106  blin2  15159  blopn  15217  xmettxlem  15236  xmettx  15237  elcncf2  15301  cncfmet  15319  cncfmptc  15323  cncfmptid  15324  negcncf  15332  mulcncflem  15334  cnrehmeocntop  15337  dedekindeulemuub  15344  dedekindeulemlu  15348  suplociccreex  15351  suplociccex  15352  dedekindicclemuub  15353  dedekindicclemlu  15357  dedekindicclemeu  15358  dedekindicclemicc  15359  ivthinclemlopn  15363  ivthinclemuopn  15365  ivthdec  15371  limcimolemlt  15391  cnplimcim  15394  cnplimclemle  15395  cnplimclemr  15396  cnlimci  15400  limccnpcntop  15402  limccnp2lem  15403  limccnp2cntop  15404  dvlemap  15407  dvfgg  15415  dvidsslem  15420  dvconstss  15425  dvcnp2cntop  15426  dvaddxxbr  15428  dvmulxxbr  15429  dvcoapbr  15434  dvcjbr  15435  plyf  15464  plycolemc  15485  dvply2g  15493  reeff1olem  15498  lgsquadlem3  15811  upgrex  15957  upgr1een  15978  subgruhgredgdm  16124  1hegrvtxdg1fi  16163  wlkvtxiedg  16199  wlkvtxiedgg  16200  sssneq  16624