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  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  11115  swrdclg  11235  fimaxre2  11792  summodclem2a  11947  fsum3cvg3  11962  fsumcl2lem  11964  fsum0diaglem  12006  fsumiun  12043  prodmodclem2a  12142  fprodcl2lem  12171  fprodap0  12187  fprodrec  12195  fprodap0f  12202  fprodle  12206  bitsfzolem  12520  bitsfzo  12521  uzwodc  12613  4sqlemffi  12974  ennnfonelemhom  13041  exmidunben  13052  ctiunctlemfo  13065  nninfdclemcl  13074  nninfdclemp1  13076  nninfdclemlt  13077  nninfdclemf1  13078  unbendc  13080  strsetsid  13120  strslssd  13134  gsumpropd2  13481  gsumress  13483  resmhm  13575  mhmima  13579  grpidssd  13664  grpinvssd  13665  mulgnnsubcl  13726  mulgnn0subcl  13727  mulgsubcl  13728  mulgpropdg  13756  submmulg  13758  subg0  13772  subgsubcl  13777  subgsub  13778  subgmulg  13780  issubg4m  13785  nsgconj  13798  ssnmz  13803  ghmnsgima  13860  subgabl  13924  rdivmuldivd  14164  rhmunitinv  14198  subrguss  14256  subrginv  14257  subrgdv  14258  lsselg  14381  islss3  14399  lspsnel3  14425  lsspropdg  14451  rnglidlmcl  14500  znf1o  14671  topssnei  14892  cnprcl2k  14936  cnss1  14956  cnptopresti  14968  cnptoprest  14969  lmres  14978  txopn  14995  txcnp  15001  xmetres2  15109  blin2  15162  blopn  15220  xmettxlem  15239  xmettx  15240  elcncf2  15304  cncfmet  15322  cncfmptc  15326  cncfmptid  15327  negcncf  15335  mulcncflem  15337  cnrehmeocntop  15340  dedekindeulemuub  15347  dedekindeulemlu  15351  suplociccreex  15354  suplociccex  15355  dedekindicclemuub  15356  dedekindicclemlu  15360  dedekindicclemeu  15361  dedekindicclemicc  15362  ivthinclemlopn  15366  ivthinclemuopn  15368  ivthdec  15374  limcimolemlt  15394  cnplimcim  15397  cnplimclemle  15398  cnplimclemr  15399  cnlimci  15403  limccnpcntop  15405  limccnp2lem  15406  limccnp2cntop  15407  dvlemap  15410  dvfgg  15418  dvidsslem  15423  dvconstss  15428  dvcnp2cntop  15429  dvaddxxbr  15431  dvmulxxbr  15432  dvcoapbr  15437  dvcjbr  15438  plyf  15467  plycolemc  15488  dvply2g  15496  reeff1olem  15501  lgsquadlem3  15814  upgrex  15960  upgr1een  15981  subgruhgredgdm  16127  1hegrvtxdg1fi  16166  wlkvtxiedg  16202  wlkvtxiedgg  16203  sssneq  16629