Theorem sseldd 3154

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

Syntax hints:   -> wi 4   e. wcel 2146   C_ wss 3127

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 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-11 1504  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-in 3133  df-ss 3140

This theorem is referenced by:  disjiun  3993  exmid01  4193  frirrg  4344  ordtri2or2exmid  4564  ontri2orexmidim  4565  riotass  5848  tfrcldm  6354  nntr2  6494  eroveu  6616  eroprf  6618  ixpssmapg  6718  findcard2d  6881  findcard2sd  6882  fimax2gtrilemstep  6890  undifdc  6913  fisseneq  6921  fidcenumlemrks  6942  fidcenumlemr  6944  fiuni  6967  suplub2ti  6990  ctssdclemn0  7099  acfun  7196  ccfunen  7238  nnppipi  7317  archnqq  7391  prarloclemlt  7467  suplocexprlemrl  7691  suplocexprlemmu  7692  suplocexprlemdisj  7694  suplocexprlemloc  7695  suplocexprlemex  7696  suplocexprlemub  7697  suplocexprlemlub  7698  suplocsrlemb  7780  suplocsrlempr  7781  suplocsrlem  7782  axpre-suploclemres  7875  suprubex  8879  suprzclex  9322  infregelbex  9569  fzssp1  10035  elfzoelz  10115  fzofzp1  10195  fzostep1  10205  frecuzrdgg  10384  frecuzrdgdomlem  10385  frecuzrdgsuctlem  10391  ser3mono  10446  bcm1k  10706  fimaxq  10773  leisorel  10783  zfz1isolemiso  10785  seq3coll  10788  fimaxre2  11201  summodclem2a  11355  fsum3cvg3  11370  fsumcl2lem  11372  fsum0diaglem  11414  fsumiun  11451  prodmodclem2a  11550  fprodcl2lem  11579  fprodap0  11595  fprodrec  11603  fprodap0f  11610  fprodle  11614  zssinfcl  11914  suprzubdc  11918  zsupssdc  11920  suprzcl2dc  11921  uzwodc  12003  ennnfonelemhom  12381  exmidunben  12392  ctiunctlemfo  12405  nninfdclemcl  12414  nninfdclemp1  12416  nninfdclemlt  12417  nninfdclemf1  12418  unbendc  12420  strsetsid  12460  strslssd  12473  mhmima  12735  grpidssd  12805  grpinvssd  12806  mulgnnsubcl  12854  mulgnn0subcl  12855  mulgsubcl  12856  mulgpropdg  12883  topssnei  13231  cnprcl2k  13275  cnss1  13295  cnptopresti  13307  cnptoprest  13308  lmres  13317  txopn  13334  txcnp  13340  xmetres2  13448  blin2  13501  blopn  13559  xmettxlem  13578  xmettx  13579  elcncf2  13630  cncfmet  13648  cncfmptc  13651  cncfmptid  13652  negcncf  13657  mulcncflem  13659  cnrehmeocntop  13662  dedekindeulemuub  13664  dedekindeulemlu  13668  suplociccreex  13671  suplociccex  13672  dedekindicclemuub  13673  dedekindicclemlu  13677  dedekindicclemeu  13678  dedekindicclemicc  13679  ivthinclemlopn  13683  ivthinclemuopn  13685  ivthdec  13691  limcimolemlt  13702  cnplimcim  13705  cnplimclemle  13706  cnplimclemr  13707  cnlimci  13711  limccnpcntop  13713  limccnp2lem  13714  limccnp2cntop  13715  dvlemap  13718  dvfgg  13726  dvcnp2cntop  13732  dvaddxxbr  13734  dvmulxxbr  13735  dvcoapbr  13740  dvcjbr  13741  reeff1olem  13761  sssneq  14310