Theorem sseldd 3226

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

Syntax hints:   -> wi 4   e. wcel 2200   C_ wss 3198

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3204  df-ss 3211

This theorem is referenced by:  disjiun  4081  exmid01  4286  frirrg  4445  ordtri2or2exmid  4667  ontri2orexmidim  4668  riotass  5996  elovimad  6057  tfrcldm  6524  nntr2  6666  eroveu  6790  eroprf  6792  ixpssmapg  6892  findcard2d  7073  findcard2sd  7074  fimax2gtrilemstep  7083  elssdc  7087  eqsndc  7088  undifdc  7109  fisseneq  7119  fidcenumlemrks  7143  fidcenumlemr  7145  fiuni  7168  suplub2ti  7191  ctssdclemn0  7300  acfun  7412  ccfunen  7473  nnppipi  7553  archnqq  7627  prarloclemlt  7703  suplocexprlemrl  7927  suplocexprlemmu  7928  suplocexprlemdisj  7930  suplocexprlemloc  7931  suplocexprlemex  7932  suplocexprlemub  7933  suplocexprlemlub  7934  suplocsrlemb  8016  suplocsrlempr  8017  suplocsrlem  8018  axpre-suploclemres  8111  suprubex  9121  suprzclex  9568  infregelbex  9822  fzssp1  10292  elfzoelz  10372  fzofzp1  10462  fzostep1  10473  zssinfcl  10482  suprzubdc  10486  zsupssdc  10488  suprzcl2dc  10489  frecuzrdgg  10668  frecuzrdgdomlem  10669  frecuzrdgsuctlem  10675  ser3mono  10739  seqf1oglem2a  10770  seqf1oglem2  10772  bcm1k  11012  fimaxq  11081  leisorel  11091  zfz1isolemiso  11093  seq3coll  11096  fun2dmnop0  11101  swrdclg  11221  fimaxre2  11778  summodclem2a  11932  fsum3cvg3  11947  fsumcl2lem  11949  fsum0diaglem  11991  fsumiun  12028  prodmodclem2a  12127  fprodcl2lem  12156  fprodap0  12172  fprodrec  12180  fprodap0f  12187  fprodle  12191  bitsfzolem  12505  bitsfzo  12506  uzwodc  12598  4sqlemffi  12959  ennnfonelemhom  13026  exmidunben  13037  ctiunctlemfo  13050  nninfdclemcl  13059  nninfdclemp1  13061  nninfdclemlt  13062  nninfdclemf1  13063  unbendc  13065  strsetsid  13105  strslssd  13119  gsumpropd2  13466  gsumress  13468  resmhm  13560  mhmima  13564  grpidssd  13649  grpinvssd  13650  mulgnnsubcl  13711  mulgnn0subcl  13712  mulgsubcl  13713  mulgpropdg  13741  submmulg  13743  subg0  13757  subgsubcl  13762  subgsub  13763  subgmulg  13765  issubg4m  13770  nsgconj  13783  ssnmz  13788  ghmnsgima  13845  subgabl  13909  rdivmuldivd  14148  rhmunitinv  14182  subrguss  14240  subrginv  14241  subrgdv  14242  lsselg  14365  islss3  14383  lspsnel3  14409  lsspropdg  14435  rnglidlmcl  14484  znf1o  14655  topssnei  14876  cnprcl2k  14920  cnss1  14940  cnptopresti  14952  cnptoprest  14953  lmres  14962  txopn  14979  txcnp  14985  xmetres2  15093  blin2  15146  blopn  15204  xmettxlem  15223  xmettx  15224  elcncf2  15288  cncfmet  15306  cncfmptc  15310  cncfmptid  15311  negcncf  15319  mulcncflem  15321  cnrehmeocntop  15324  dedekindeulemuub  15331  dedekindeulemlu  15335  suplociccreex  15338  suplociccex  15339  dedekindicclemuub  15340  dedekindicclemlu  15344  dedekindicclemeu  15345  dedekindicclemicc  15346  ivthinclemlopn  15350  ivthinclemuopn  15352  ivthdec  15358  limcimolemlt  15378  cnplimcim  15381  cnplimclemle  15382  cnplimclemr  15383  cnlimci  15387  limccnpcntop  15389  limccnp2lem  15390  limccnp2cntop  15391  dvlemap  15394  dvfgg  15402  dvidsslem  15407  dvconstss  15412  dvcnp2cntop  15413  dvaddxxbr  15415  dvmulxxbr  15416  dvcoapbr  15421  dvcjbr  15422  plyf  15451  plycolemc  15472  dvply2g  15480  reeff1olem  15485  lgsquadlem3  15798  upgrex  15944  wlkvtxiedg  16142  wlkvtxiedgg  16143  sssneq  16539