Theorem sseldd 3249

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 3247	. 2 |- ( ph -> ( C e. A -> C e. B ) )
4	1, 3	mpd 13	1 |- ( ph -> C e. B )

Syntax hints:   -> wi 4   e. wcel 2209   C_ 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  4120  exmid01  4330  frirrg  4490  ordtri2or2exmid  4713  ontri2orexmidim  4714  riotass  6058  elovimad  6119  funsssuppss  6488  suppssfvg  6493  tfrcldm  6624  nntr2  6766  eroveu  6890  eroprf  6892  ixpssmapg  7000  findcard2d  7185  findcard2sd  7186  fimax2gtrilemstep  7195  elssdc  7199  eqsndc  7200  undifdc  7221  fisseneq  7232  fissfi  7253  fidcenumlemrks  7260  fidcenumlemr  7262  fiuni  7302  suplub2ti  7331  ctssdclemn0  7440  acfun  7553  ccfunen  7620  nnppipi  7700  archnqq  7774  prarloclemlt  7850  suplocexprlemrl  8074  suplocexprlemmu  8075  suplocexprlemdisj  8077  suplocexprlemloc  8078  suplocexprlemex  8079  suplocexprlemub  8080  suplocexprlemlub  8081  suplocsrlemb  8163  suplocsrlempr  8164  suplocsrlem  8165  axpre-suploclemres  8258  suprubex  9271  suprzclex  9723  infregelbex  9977  fzssp1  10451  elfzoelz  10532  fzofzp1  10623  fzostep1  10634  zssinfcl  10643  suprzubdc  10649  zsupssdc  10651  suprzcl2dc  10652  frecuzrdgg  10831  frecuzrdgdomlem  10832  frecuzrdgsuctlem  10838  ser3mono  10902  seqf1oglem2a  10933  seqf1oglem2  10935  bcm1k  11176  fimaxq  11248  leisorel  11267  zfz1isolemiso  11269  seq3coll  11272  fun2dmnop0  11280  swrdclg  11400  fimaxre2  11971  summodclem2a  12126  fsum3cvg3  12141  fsumcl2lem  12143  fsum0diaglem  12185  fsumiun  12222  prodmodclem2a  12321  fprodcl2lem  12350  fprodap0  12366  fprodrec  12374  fprodap0f  12381  fprodle  12385  bitsfzolem  12699  bitsfzo  12700  uzwodc  12792  4sqlemffi  13153  ballotfilemcdc  13201  ballotfilemsdom  13233  ballotfilemfrceq  13250  ennnfonelemhom  13284  exmidunben  13295  ctiunctlemfo  13308  nninfdclemcl  13317  nninfdclemp1  13319  nninfdclemlt  13320  nninfdclemf1  13321  unbendc  13323  strsetsid  13363  strslssd  13377  gzsumress  13689  resmhm  13771  mhmima  13775  grpidssd  13858  grpinvssd  13859  mulgnnsubcl  13914  mulgnn0subcl  13915  mulgsubcl  13916  mulgpropdg  13944  submmulg  13946  subg0  13960  subgsubcl  13965  subgsub  13966  subgmulg  13968  issubg4m  13973  nsgconj  13986  ssnmz  13991  ghmnsgima  14048  cmnsubm  14089  subgabl  14113  rdivmuldivd  14424  rhmunitinv  14458  subrguss  14517  subrginv  14518  subrgdv  14519  lsselg  14670  islss3  14688  lspsnel3  14714  lsspropdg  14740  rnglidlmcl  14789  znf1o  14958  topssnei  15186  cnprcl2k  15230  cnss1  15250  cnptopresti  15262  cnptoprest  15263  lmres  15272  txopn  15289  txcnp  15295  xmetres2  15403  blin2  15456  blopn  15514  xmettxlem  15533  xmettx  15534  elcncf2  15598  cncfmet  15616  cncfmptc  15620  cncfmptid  15621  negcncf  15629  mulcncflem  15631  cnrehmeocntop  15634  dedekindeulemuub  15641  dedekindeulemlu  15645  suplociccreex  15648  suplociccex  15649  dedekindicclemuub  15650  dedekindicclemlu  15654  dedekindicclemeu  15655  dedekindicclemicc  15656  ivthinclemlopn  15660  ivthinclemuopn  15662  ivthdec  15668  limcimolemlt  15688  cnplimcim  15691  cnplimclemle  15692  cnplimclemr  15693  cnlimci  15697  limccnpcntop  15699  limccnp2lem  15700  limccnp2cntop  15701  dvlemap  15704  dvfgg  15712  dvidsslem  15717  dvconstss  15722  dvcnp2cntop  15723  dvaddxxbr  15725  dvmulxxbr  15726  dvcoapbr  15731  dvcjbr  15732  plyf  15761  plycolemc  15782  dvply2g  15790  reeff1olem  15795  lgsquadlem3  16112  upgrex  16258  upgr1een  16279  subgruhgredgdm  16425  1hegrvtxdg1fi  16464  wlkvtxiedg  16500  wlkvtxiedgg  16501  sssneq  16946