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  9283  ind1  9302  suprzclex  9748  infregelbex  10007  fzssp1  10483  elfzoelz  10564  fzofzp1  10655  fzostep1  10666  zssinfcl  10675  suprzubdc  10681  zsupssdc  10683  suprzcl2dc  10684  frecuzrdgg  10866  frecuzrdgdomlem  10867  frecuzrdgsuctlem  10873  ser3mono  10937  seqf1oglem2a  10968  seqf1oglem2  10970  bcm1k  11212  fimaxq  11284  leisorel  11303  zfz1isolemiso  11305  seq3coll  11308  fun2dmnop0  11316  swrdclg  11436  fimaxre2  12008  summodclem2a  12164  fsum3cvg3  12179  fsumcl2lem  12181  fsum0diaglem  12223  fsumiun  12260  prodmodclem2a  12359  fprodcl2lem  12388  fprodap0  12404  fprodrec  12412  fprodap0f  12419  fprodle  12423  bitsfzolem  12737  bitsfzo  12738  uzwodc  12830  4sqlemffi  13195  ballotfilemcdc  13272  ballotfilemsdom  13304  ballotfilemfrceq  13321  ennnfonelemhom  13355  exmidunben  13366  ctiunctlemfo  13379  nninfdclemcl  13388  nninfdclemp1  13390  nninfdclemlt  13391  nninfdclemf1  13392  unbendc  13394  strsetsid  13434  strslssd  13448  gzsumress  13761  resmhm  13843  mhmima  13847  grpidssd  13930  grpinvssd  13931  mulgnnsubcl  13986  mulgnn0subcl  13987  mulgsubcl  13988  mulgpropdg  14016  submmulg  14018  subg0  14032  subgsubcl  14037  subgsub  14038  subgmulg  14040  issubg4m  14045  nsgconj  14058  ssnmz  14063  ghmnsgima  14120  cmnsubm  14161  subgabl  14185  rdivmuldivd  14500  rhmunitinv  14534  subrguss  14593  subrginv  14594  subrgdv  14595  lsselg  14747  islss3  14765  ellspsn3  14791  lsspropdg  14817  rnglidlmcl  14866  znf1o  15035  issubassa2  15084  topssnei  15312  cnprcl2k  15356  cnss1  15376  cnptopresti  15388  cnptoprest  15389  lmres  15398  txopn  15415  txcnp  15421  xmetres2  15529  blin2  15582  blopn  15640  xmettxlem  15659  xmettx  15660  elcncf2  15724  cncfmet  15742  cncfmptc  15746  cncfmptid  15747  negcncf  15755  mulcncflem  15757  cnrehmeocntop  15760  dedekindeulemuub  15767  dedekindeulemlu  15771  suplociccreex  15774  suplociccex  15775  dedekindicclemuub  15776  dedekindicclemlu  15780  dedekindicclemeu  15781  dedekindicclemicc  15782  ivthinclemlopn  15786  ivthinclemuopn  15788  ivthdec  15794  limcimolemlt  15814  cnplimcim  15817  cnplimclemle  15818  cnplimclemr  15819  cnlimci  15823  limccnpcntop  15825  limccnp2lem  15826  limccnp2cntop  15827  dvlemap  15830  dvfgg  15838  dvidsslem  15843  dvconstss  15848  dvcnp2cntop  15849  dvaddxxbr  15851  dvmulxxbr  15852  dvcoapbr  15857  dvcjbr  15858  plyf  15887  plycolemc  15908  dvply2g  15916  reeff1olem  15921  lgsquadlem3  16296  upgrex  16442  upgr1een  16463  subgruhgredgdm  16609  1hegrvtxdg1fi  16648  wlkvtxiedg  16684  wlkvtxiedgg  16685  sssneq  17130