Theorem sseldd 3228

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

Hypotheses

Ref	Expression
sseld.1	|- ( ph -> A C_ B )
sseldd.2	|- ( ph -> C e. A )

Assertion

Ref	Expression
sseldd	|- ( ph -> C e. B )

Proof of Theorem sseldd

Step	Hyp	Ref	Expression
1		sseldd.2	. 2 |- ( ph -> C e. A )
2		sseld.1	. . 3 |- ( ph -> A C_ B )
3	2	sseld 3226	. 2 |- ( ph -> ( C e. A -> C e. B ) )
4	1, 3	mpd 13	1 |- ( ph -> C e. B )

Syntax hints:   -> wi 4   e. wcel 2202   C_ 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  6000  elovimad  6061  tfrcldm  6528  nntr2  6670  eroveu  6794  eroprf  6796  ixpssmapg  6896  findcard2d  7079  findcard2sd  7080  fimax2gtrilemstep  7089  elssdc  7093  eqsndc  7094  undifdc  7115  fisseneq  7126  fidcenumlemrks  7151  fidcenumlemr  7153  fiuni  7176  suplub2ti  7199  ctssdclemn0  7308  acfun  7421  ccfunen  7482  nnppipi  7562  archnqq  7636  prarloclemlt  7712  suplocexprlemrl  7936  suplocexprlemmu  7937  suplocexprlemdisj  7939  suplocexprlemloc  7940  suplocexprlemex  7941  suplocexprlemub  7942  suplocexprlemlub  7943  suplocsrlemb  8025  suplocsrlempr  8026  suplocsrlem  8027  axpre-suploclemres  8120  suprubex  9130  suprzclex  9577  infregelbex  9831  fzssp1  10301  elfzoelz  10381  fzofzp1  10471  fzostep1  10482  zssinfcl  10491  suprzubdc  10495  zsupssdc  10497  suprzcl2dc  10498  frecuzrdgg  10677  frecuzrdgdomlem  10678  frecuzrdgsuctlem  10684  ser3mono  10748  seqf1oglem2a  10779  seqf1oglem2  10781  bcm1k  11021  fimaxq  11090  leisorel  11100  zfz1isolemiso  11102  seq3coll  11105  fun2dmnop0  11110  swrdclg  11230  fimaxre2  11787  summodclem2a  11941  fsum3cvg3  11956  fsumcl2lem  11958  fsum0diaglem  12000  fsumiun  12037  prodmodclem2a  12136  fprodcl2lem  12165  fprodap0  12181  fprodrec  12189  fprodap0f  12196  fprodle  12200  bitsfzolem  12514  bitsfzo  12515  uzwodc  12607  4sqlemffi  12968  ennnfonelemhom  13035  exmidunben  13046  ctiunctlemfo  13059  nninfdclemcl  13068  nninfdclemp1  13070  nninfdclemlt  13071  nninfdclemf1  13072  unbendc  13074  strsetsid  13114  strslssd  13128  gsumpropd2  13475  gsumress  13477  resmhm  13569  mhmima  13573  grpidssd  13658  grpinvssd  13659  mulgnnsubcl  13720  mulgnn0subcl  13721  mulgsubcl  13722  mulgpropdg  13750  submmulg  13752  subg0  13766  subgsubcl  13771  subgsub  13772  subgmulg  13774  issubg4m  13779  nsgconj  13792  ssnmz  13797  ghmnsgima  13854  subgabl  13918  rdivmuldivd  14157  rhmunitinv  14191  subrguss  14249  subrginv  14250  subrgdv  14251  lsselg  14374  islss3  14392  lspsnel3  14418  lsspropdg  14444  rnglidlmcl  14493  znf1o  14664  topssnei  14885  cnprcl2k  14929  cnss1  14949  cnptopresti  14961  cnptoprest  14962  lmres  14971  txopn  14988  txcnp  14994  xmetres2  15102  blin2  15155  blopn  15213  xmettxlem  15232  xmettx  15233  elcncf2  15297  cncfmet  15315  cncfmptc  15319  cncfmptid  15320  negcncf  15328  mulcncflem  15330  cnrehmeocntop  15333  dedekindeulemuub  15340  dedekindeulemlu  15344  suplociccreex  15347  suplociccex  15348  dedekindicclemuub  15349  dedekindicclemlu  15353  dedekindicclemeu  15354  dedekindicclemicc  15355  ivthinclemlopn  15359  ivthinclemuopn  15361  ivthdec  15367  limcimolemlt  15387  cnplimcim  15390  cnplimclemle  15391  cnplimclemr  15392  cnlimci  15396  limccnpcntop  15398  limccnp2lem  15399  limccnp2cntop  15400  dvlemap  15403  dvfgg  15411  dvidsslem  15416  dvconstss  15421  dvcnp2cntop  15422  dvaddxxbr  15424  dvmulxxbr  15425  dvcoapbr  15430  dvcjbr  15431  plyf  15460  plycolemc  15481  dvply2g  15489  reeff1olem  15494  lgsquadlem3  15807  upgrex  15953  upgr1een  15974  subgruhgredgdm  16120  1hegrvtxdg1fi  16159  wlkvtxiedg  16195  wlkvtxiedgg  16196  sssneq  16603