Theorem sseldd 3098

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

Syntax hints:   -> wi 4   e. wcel 1480   C_ wss 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-in 3077  df-ss 3084

This theorem is referenced by:  disjiun  3924  exmid01  4121  frirrg  4272  ordtri2or2exmid  4486  riotass  5757  tfrcldm  6260  nntr2  6399  eroveu  6520  eroprf  6522  ixpssmapg  6622  findcard2d  6785  findcard2sd  6786  fimax2gtrilemstep  6794  undifdc  6812  fisseneq  6820  fidcenumlemrks  6841  fidcenumlemr  6843  fiuni  6866  suplub2ti  6888  ctssdclemn0  6995  acfun  7063  ccfunen  7079  nnppipi  7151  archnqq  7225  prarloclemlt  7301  suplocexprlemrl  7525  suplocexprlemmu  7526  suplocexprlemdisj  7528  suplocexprlemloc  7529  suplocexprlemex  7530  suplocexprlemub  7531  suplocexprlemlub  7532  suplocsrlemb  7614  suplocsrlempr  7615  suplocsrlem  7616  axpre-suploclemres  7709  suprubex  8709  suprzclex  9149  fzssp1  9847  elfzoelz  9924  fzofzp1  10004  fzostep1  10014  frecuzrdgg  10189  frecuzrdgdomlem  10190  frecuzrdgsuctlem  10196  ser3mono  10251  bcm1k  10506  fimaxq  10573  leisorel  10580  zfz1isolemiso  10582  seq3coll  10585  fimaxre2  10998  summodclem2a  11150  fsum3cvg3  11165  fsumcl2lem  11167  fsum0diaglem  11209  fsumiun  11246  prodmodclem2a  11345  zssinfcl  11641  ennnfonelemhom  11928  exmidunben  11939  ctiunctlemfo  11952  strsetsid  11992  strslssd  12005  topssnei  12331  cnprcl2k  12375  cnss1  12395  cnptopresti  12407  cnptoprest  12408  lmres  12417  txopn  12434  txcnp  12440  xmetres2  12548  blin2  12601  blopn  12659  xmettxlem  12678  xmettx  12679  elcncf2  12730  cncfmet  12748  cncfmptc  12751  cncfmptid  12752  negcncf  12757  mulcncflem  12759  cnrehmeocntop  12762  dedekindeulemuub  12764  dedekindeulemlu  12768  suplociccreex  12771  suplociccex  12772  dedekindicclemuub  12773  dedekindicclemlu  12777  dedekindicclemeu  12778  dedekindicclemicc  12779  ivthinclemlopn  12783  ivthinclemuopn  12785  ivthdec  12791  limcimolemlt  12802  cnplimcim  12805  cnplimclemle  12806  cnplimclemr  12807  cnlimci  12811  limccnpcntop  12813  limccnp2lem  12814  limccnp2cntop  12815  dvlemap  12818  dvfgg  12826  dvcnp2cntop  12832  dvaddxxbr  12834  dvmulxxbr  12835  dvcoapbr  12840  dvcjbr  12841