Theorem sseldd 3138

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

Syntax hints:   -> wi 4   e. wcel 2135   C_ wss 3111

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 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-11 1493  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-in 3117  df-ss 3124

This theorem is referenced by:  disjiun  3971  exmid01  4171  frirrg  4322  ordtri2or2exmid  4542  ontri2orexmidim  4543  riotass  5819  tfrcldm  6322  nntr2  6462  eroveu  6583  eroprf  6585  ixpssmapg  6685  findcard2d  6848  findcard2sd  6849  fimax2gtrilemstep  6857  undifdc  6880  fisseneq  6888  fidcenumlemrks  6909  fidcenumlemr  6911  fiuni  6934  suplub2ti  6957  ctssdclemn0  7066  acfun  7154  ccfunen  7196  nnppipi  7275  archnqq  7349  prarloclemlt  7425  suplocexprlemrl  7649  suplocexprlemmu  7650  suplocexprlemdisj  7652  suplocexprlemloc  7653  suplocexprlemex  7654  suplocexprlemub  7655  suplocexprlemlub  7656  suplocsrlemb  7738  suplocsrlempr  7739  suplocsrlem  7740  axpre-suploclemres  7833  suprubex  8837  suprzclex  9280  infregelbex  9527  fzssp1  9992  elfzoelz  10072  fzofzp1  10152  fzostep1  10162  frecuzrdgg  10341  frecuzrdgdomlem  10342  frecuzrdgsuctlem  10348  ser3mono  10403  bcm1k  10662  fimaxq  10729  leisorel  10736  zfz1isolemiso  10738  seq3coll  10741  fimaxre2  11154  summodclem2a  11308  fsum3cvg3  11323  fsumcl2lem  11325  fsum0diaglem  11367  fsumiun  11404  prodmodclem2a  11503  fprodcl2lem  11532  fprodap0  11548  fprodrec  11556  fprodap0f  11563  fprodle  11567  zssinfcl  11866  suprzubdc  11870  zsupssdc  11872  suprzcl2dc  11873  ennnfonelemhom  12285  exmidunben  12296  ctiunctlemfo  12309  nninfdclemcl  12320  nninfdclemp1  12322  nninfdclemlt  12323  nninfdclemf1  12324  unbendc  12326  strsetsid  12364  strslssd  12377  topssnei  12703  cnprcl2k  12747  cnss1  12767  cnptopresti  12779  cnptoprest  12780  lmres  12789  txopn  12806  txcnp  12812  xmetres2  12920  blin2  12973  blopn  13031  xmettxlem  13050  xmettx  13051  elcncf2  13102  cncfmet  13120  cncfmptc  13123  cncfmptid  13124  negcncf  13129  mulcncflem  13131  cnrehmeocntop  13134  dedekindeulemuub  13136  dedekindeulemlu  13140  suplociccreex  13143  suplociccex  13144  dedekindicclemuub  13145  dedekindicclemlu  13149  dedekindicclemeu  13150  dedekindicclemicc  13151  ivthinclemlopn  13155  ivthinclemuopn  13157  ivthdec  13163  limcimolemlt  13174  cnplimcim  13177  cnplimclemle  13178  cnplimclemr  13179  cnlimci  13183  limccnpcntop  13185  limccnp2lem  13186  limccnp2cntop  13187  dvlemap  13190  dvfgg  13198  dvcnp2cntop  13204  dvaddxxbr  13206  dvmulxxbr  13207  dvcoapbr  13212  dvcjbr  13213  reeff1olem  13233  sssneq  13716