Theorem sseldd 3249

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   C_ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  disjiun  4125  exmid01  4335  frirrg  4495  ordtri2or2exmid  4718  ontri2orexmidim  4719  riotass  6068  elovimad  6129  funsssuppss  6498  suppssfvg  6503  tfrcldm  6634  nntr2  6776  eroveu  6900  eroprf  6902  ixpssmapg  7010  findcard2d  7195  findcard2sd  7196  fimax2gtrilemstep  7205  elssdc  7209  eqsndc  7210  undifdc  7231  fisseneq  7242  fissfi  7263  fidcenumlemrks  7270  fidcenumlemr  7272  fiuni  7312  suplub2ti  7341  ctssdclemn0  7450  acfun  7563  ccfunen  7630  nnppipi  7710  archnqq  7784  prarloclemlt  7860  suplocexprlemrl  8084  suplocexprlemmu  8085  suplocexprlemdisj  8087  suplocexprlemloc  8088  suplocexprlemex  8089  suplocexprlemub  8090  suplocexprlemlub  8091  suplocsrlemb  8173  suplocsrlempr  8174  suplocsrlem  8175  axpre-suploclemres  8268  suprubex  9281  ind1  9300  suprzclex  9744  infregelbex  9998  fzssp1  10473  elfzoelz  10554  fzofzp1  10645  fzostep1  10656  zssinfcl  10665  suprzubdc  10671  zsupssdc  10673  suprzcl2dc  10674  frecuzrdgg  10853  frecuzrdgdomlem  10854  frecuzrdgsuctlem  10860  ser3mono  10924  seqf1oglem2a  10955  seqf1oglem2  10957  bcm1k  11198  fimaxq  11270  leisorel  11289  zfz1isolemiso  11291  seq3coll  11294  fun2dmnop0  11302  swrdclg  11422  fimaxre2  11993  summodclem2a  12148  fsum3cvg3  12163  fsumcl2lem  12165  fsum0diaglem  12207  fsumiun  12244  prodmodclem2a  12343  fprodcl2lem  12372  fprodap0  12388  fprodrec  12396  fprodap0f  12403  fprodle  12407  bitsfzolem  12721  bitsfzo  12722  uzwodc  12814  4sqlemffi  13175  ballotfilemcdc  13223  ballotfilemsdom  13255  ballotfilemfrceq  13272  ennnfonelemhom  13306  exmidunben  13317  ctiunctlemfo  13330  nninfdclemcl  13339  nninfdclemp1  13341  nninfdclemlt  13342  nninfdclemf1  13343  unbendc  13345  strsetsid  13385  strslssd  13399  gzsumress  13712  resmhm  13794  mhmima  13798  grpidssd  13881  grpinvssd  13882  mulgnnsubcl  13937  mulgnn0subcl  13938  mulgsubcl  13939  mulgpropdg  13967  submmulg  13969  subg0  13983  subgsubcl  13988  subgsub  13989  subgmulg  13991  issubg4m  13996  nsgconj  14009  ssnmz  14014  ghmnsgima  14071  cmnsubm  14112  subgabl  14136  rdivmuldivd  14451  rhmunitinv  14485  subrguss  14544  subrginv  14545  subrgdv  14546  lsselg  14698  islss3  14716  ellspsn3  14742  lsspropdg  14768  rnglidlmcl  14817  znf1o  14986  issubassa2  15035  topssnei  15263  cnprcl2k  15307  cnss1  15327  cnptopresti  15339  cnptoprest  15340  lmres  15349  txopn  15366  txcnp  15372  xmetres2  15480  blin2  15533  blopn  15591  xmettxlem  15610  xmettx  15611  elcncf2  15675  cncfmet  15693  cncfmptc  15697  cncfmptid  15698  negcncf  15706  mulcncflem  15708  cnrehmeocntop  15711  dedekindeulemuub  15718  dedekindeulemlu  15722  suplociccreex  15725  suplociccex  15726  dedekindicclemuub  15727  dedekindicclemlu  15731  dedekindicclemeu  15732  dedekindicclemicc  15733  ivthinclemlopn  15737  ivthinclemuopn  15739  ivthdec  15745  limcimolemlt  15765  cnplimcim  15768  cnplimclemle  15769  cnplimclemr  15770  cnlimci  15774  limccnpcntop  15776  limccnp2lem  15777  limccnp2cntop  15778  dvlemap  15781  dvfgg  15789  dvidsslem  15794  dvconstss  15799  dvcnp2cntop  15800  dvaddxxbr  15802  dvmulxxbr  15803  dvcoapbr  15808  dvcjbr  15809  plyf  15838  plycolemc  15859  dvply2g  15867  reeff1olem  15872  lgsquadlem3  16198  upgrex  16344  upgr1een  16365  subgruhgredgdm  16511  1hegrvtxdg1fi  16550  wlkvtxiedg  16586  wlkvtxiedgg  16587  sssneq  17032