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  4337  frirrg  4497  ordtri2or2exmid  4720  ontri2orexmidim  4721  riotass  6071  elovimad  6132  funsssuppss  6502  suppssfvg  6507  tfrcldm  6639  nntr2  6781  eroveu  6905  eroprf  6907  ixpssmapg  7016  findcard2d  7201  findcard2sd  7202  fimax2gtrilemstep  7211  elssdc  7215  eqsndc  7216  undifdc  7237  fisseneq  7248  fissfi  7269  fidcenumlemrks  7277  fidcenumlemr  7279  funisfsuppdc  7298  fiuni  7317  suplub2ti  7347  ctssdclemn0  7456  acfun  7569  ccfunen  7636  nnppipi  7716  archnqq  7790  prarloclemlt  7866  suplocexprlemrl  8090  suplocexprlemmu  8091  suplocexprlemdisj  8093  suplocexprlemloc  8094  suplocexprlemex  8095  suplocexprlemub  8096  suplocexprlemlub  8097  suplocsrlemb  8179  suplocsrlempr  8180  suplocsrlem  8181  axpre-suploclemres  8274  suprubex  9289  ind1  9309  suprzclex  9754  infregelbex  10013  fzssp1  10489  elfzoelz  10570  fzofzp1  10661  fzostep1  10672  zssinfcl  10681  suprzubdc  10687  zsupssdc  10689  suprzcl2dc  10690  frecuzrdgg  10873  frecuzrdgdomlem  10874  frecuzrdgsuctlem  10880  ser3mono  10944  seqf1oglem2a  10975  seqf1oglem2  10977  bcm1k  11219  fimaxq  11291  leisorel  11310  zfz1isolemiso  11312  seq3coll  11315  fun2dmnop0  11323  swrdclg  11443  fimaxre2  12015  fiidxsupcl  12017  summodclem2a  12172  fsum3cvg3  12187  fsumcl2lem  12189  fsum0diaglem  12231  fsumiun  12268  prodmodclem2a  12367  fprodcl2lem  12396  fprodap0  12412  fprodrec  12420  fprodap0f  12427  fprodle  12431  bitsfzolem  12745  bitsfzo  12746  uzwodc  12838  4sqlemffi  13203  ballotfilemcdc  13280  ballotfilemsdom  13312  ballotfilemfrceq  13329  ennnfonelemhom  13363  exmidunben  13374  ctiunctlemfo  13387  nninfdclemcl  13396  nninfdclemp1  13398  nninfdclemlt  13399  nninfdclemf1  13400  unbendc  13402  strsetsid  13442  strslssd  13456  gzsumress  13770  resmhm  13852  mhmima  13856  grpidssd  13939  grpinvssd  13940  mulgnnsubcl  13995  mulgnn0subcl  13996  mulgsubcl  13997  mulgpropdg  14025  submmulg  14027  subg0  14041  subgsubcl  14046  subgsub  14047  subgmulg  14049  issubg4m  14054  nsgconj  14067  ssnmz  14072  ghmnsgima  14129  cntzrcl  14158  cntzssv  14159  cntrsubgnsg  14174  cmnsubm  14201  subgabl  14225  gsummptfidmsplit  14253  rdivmuldivd  14559  rhmunitinv  14593  subrguss  14652  subrginv  14653  subrgdv  14654  lsselg  14806  islss3  14824  ellspsn3  14850  lsspropdg  14876  rnglidlmcl  14925  znf1o  15094  issubassa2  15143  psrbagmaxlem1  15178  mplsubgfilemcl  15232  topssnei  15405  cnprcl2k  15449  cnss1  15469  cnptopresti  15481  cnptoprest  15482  lmres  15491  txopn  15508  txcnp  15514  xmetres2  15622  blin2  15675  blopn  15733  xmettxlem  15752  xmettx  15753  elcncf2  15817  cncfmet  15835  cncfmptc  15839  cncfmptid  15840  negcncf  15848  mulcncflem  15850  cnrehmeocntop  15853  dedekindeulemuub  15860  dedekindeulemlu  15864  suplociccreex  15867  suplociccex  15868  dedekindicclemuub  15869  dedekindicclemlu  15873  dedekindicclemeu  15874  dedekindicclemicc  15875  ivthinclemlopn  15879  ivthinclemuopn  15881  ivthdec  15887  limcimolemlt  15907  cnplimcim  15910  cnplimclemle  15911  cnplimclemr  15912  cnlimci  15916  limccnpcntop  15918  limccnp2lem  15919  limccnp2cntop  15920  dvlemap  15923  dvfgg  15931  dvidsslem  15936  dvconstss  15941  dvcnp2cntop  15942  dvaddxxbr  15944  dvmulxxbr  15945  dvcoapbr  15950  dvcjbr  15951  plyf  15980  plycolemc  16001  dvply2g  16009  reeff1olem  16014  lgsquadlem3  16420  upgrex  16566  upgr1een  16587  subgruhgredgdm  16733  1hegrvtxdg1fi  16772  wlkvtxiedg  16808  wlkvtxiedgg  16809  sssneq  17254