Theorem sseldd 3249

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

Syntax hints:   → wi 4   ∈ wcel 2209   ⊆ wss 3220

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is referenced by:  disjiun  4123  exmid01  4333  frirrg  4493  ordtri2or2exmid  4716  ontri2orexmidim  4717  riotass  6062  elovimad  6123  funsssuppss  6492  suppssfvg  6497  tfrcldm  6628  nntr2  6770  eroveu  6894  eroprf  6896  ixpssmapg  7004  findcard2d  7189  findcard2sd  7190  fimax2gtrilemstep  7199  elssdc  7203  eqsndc  7204  undifdc  7225  fisseneq  7236  fissfi  7257  fidcenumlemrks  7264  fidcenumlemr  7266  fiuni  7306  suplub2ti  7335  ctssdclemn0  7444  acfun  7557  ccfunen  7624  nnppipi  7704  archnqq  7778  prarloclemlt  7854  suplocexprlemrl  8078  suplocexprlemmu  8079  suplocexprlemdisj  8081  suplocexprlemloc  8082  suplocexprlemex  8083  suplocexprlemub  8084  suplocexprlemlub  8085  suplocsrlemb  8167  suplocsrlempr  8168  suplocsrlem  8169  axpre-suploclemres  8262  suprubex  9275  suprzclex  9727  infregelbex  9981  fzssp1  10456  elfzoelz  10537  fzofzp1  10628  fzostep1  10639  zssinfcl  10648  suprzubdc  10654  zsupssdc  10656  suprzcl2dc  10657  frecuzrdgg  10836  frecuzrdgdomlem  10837  frecuzrdgsuctlem  10843  ser3mono  10907  seqf1oglem2a  10938  seqf1oglem2  10940  bcm1k  11181  fimaxq  11253  leisorel  11272  zfz1isolemiso  11274  seq3coll  11277  fun2dmnop0  11285  swrdclg  11405  fimaxre2  11976  summodclem2a  12131  fsum3cvg3  12146  fsumcl2lem  12148  fsum0diaglem  12190  fsumiun  12227  prodmodclem2a  12326  fprodcl2lem  12355  fprodap0  12371  fprodrec  12379  fprodap0f  12386  fprodle  12390  bitsfzolem  12704  bitsfzo  12705  uzwodc  12797  4sqlemffi  13158  ballotfilemcdc  13206  ballotfilemsdom  13238  ballotfilemfrceq  13255  ennnfonelemhom  13289  exmidunben  13300  ctiunctlemfo  13313  nninfdclemcl  13322  nninfdclemp1  13324  nninfdclemlt  13325  nninfdclemf1  13326  unbendc  13328  strsetsid  13368  strslssd  13382  gzsumress  13695  resmhm  13777  mhmima  13781  grpidssd  13864  grpinvssd  13865  mulgnnsubcl  13920  mulgnn0subcl  13921  mulgsubcl  13922  mulgpropdg  13950  submmulg  13952  subg0  13966  subgsubcl  13971  subgsub  13972  subgmulg  13974  issubg4m  13979  nsgconj  13992  ssnmz  13997  ghmnsgima  14054  cmnsubm  14095  subgabl  14119  rdivmuldivd  14434  rhmunitinv  14468  subrguss  14527  subrginv  14528  subrgdv  14529  lsselg  14681  islss3  14699  ellspsn3  14725  lsspropdg  14751  rnglidlmcl  14800  znf1o  14969  issubassa2  15018  topssnei  15246  cnprcl2k  15290  cnss1  15310  cnptopresti  15322  cnptoprest  15323  lmres  15332  txopn  15349  txcnp  15355  xmetres2  15463  blin2  15516  blopn  15574  xmettxlem  15593  xmettx  15594  elcncf2  15658  cncfmet  15676  cncfmptc  15680  cncfmptid  15681  negcncf  15689  mulcncflem  15691  cnrehmeocntop  15694  dedekindeulemuub  15701  dedekindeulemlu  15705  suplociccreex  15708  suplociccex  15709  dedekindicclemuub  15710  dedekindicclemlu  15714  dedekindicclemeu  15715  dedekindicclemicc  15716  ivthinclemlopn  15720  ivthinclemuopn  15722  ivthdec  15728  limcimolemlt  15748  cnplimcim  15751  cnplimclemle  15752  cnplimclemr  15753  cnlimci  15757  limccnpcntop  15759  limccnp2lem  15760  limccnp2cntop  15761  dvlemap  15764  dvfgg  15772  dvidsslem  15777  dvconstss  15782  dvcnp2cntop  15783  dvaddxxbr  15785  dvmulxxbr  15786  dvcoapbr  15791  dvcjbr  15792  plyf  15821  plycolemc  15842  dvply2g  15850  reeff1olem  15855  lgsquadlem3  16181  upgrex  16327  upgr1een  16348  subgruhgredgdm  16494  1hegrvtxdg1fi  16533  wlkvtxiedg  16569  wlkvtxiedgg  16570  sssneq  17015