Theorem sseldd 3193

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

Syntax hints:   -> wi 4   e. wcel 2175   C_ wss 3165

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-in 3171  df-ss 3178

This theorem is referenced by:  disjiun  4038  exmid01  4241  frirrg  4396  ordtri2or2exmid  4618  ontri2orexmidim  4619  riotass  5926  tfrcldm  6448  nntr2  6588  eroveu  6712  eroprf  6714  ixpssmapg  6814  findcard2d  6987  findcard2sd  6988  fimax2gtrilemstep  6996  undifdc  7020  fisseneq  7030  fidcenumlemrks  7054  fidcenumlemr  7056  fiuni  7079  suplub2ti  7102  ctssdclemn0  7211  acfun  7318  ccfunen  7375  nnppipi  7455  archnqq  7529  prarloclemlt  7605  suplocexprlemrl  7829  suplocexprlemmu  7830  suplocexprlemdisj  7832  suplocexprlemloc  7833  suplocexprlemex  7834  suplocexprlemub  7835  suplocexprlemlub  7836  suplocsrlemb  7918  suplocsrlempr  7919  suplocsrlem  7920  axpre-suploclemres  8013  suprubex  9023  suprzclex  9470  infregelbex  9718  fzssp1  10188  elfzoelz  10268  fzofzp1  10354  fzostep1  10364  zssinfcl  10373  suprzubdc  10377  zsupssdc  10379  suprzcl2dc  10380  frecuzrdgg  10559  frecuzrdgdomlem  10560  frecuzrdgsuctlem  10566  ser3mono  10630  seqf1oglem2a  10661  seqf1oglem2  10663  bcm1k  10903  fimaxq  10970  leisorel  10980  zfz1isolemiso  10982  seq3coll  10985  fun2dmnop0  10990  fimaxre2  11509  summodclem2a  11663  fsum3cvg3  11678  fsumcl2lem  11680  fsum0diaglem  11722  fsumiun  11759  prodmodclem2a  11858  fprodcl2lem  11887  fprodap0  11903  fprodrec  11911  fprodap0f  11918  fprodle  11922  bitsfzolem  12236  bitsfzo  12237  uzwodc  12329  4sqlemffi  12690  ennnfonelemhom  12757  exmidunben  12768  ctiunctlemfo  12781  nninfdclemcl  12790  nninfdclemp1  12792  nninfdclemlt  12793  nninfdclemf1  12794  unbendc  12796  strsetsid  12836  strslssd  12850  gsumpropd2  13196  gsumress  13198  resmhm  13290  mhmima  13294  grpidssd  13379  grpinvssd  13380  mulgnnsubcl  13441  mulgnn0subcl  13442  mulgsubcl  13443  mulgpropdg  13471  submmulg  13473  subg0  13487  subgsubcl  13492  subgsub  13493  subgmulg  13495  issubg4m  13500  nsgconj  13513  ssnmz  13518  ghmnsgima  13575  subgabl  13639  rdivmuldivd  13877  rhmunitinv  13911  subrguss  13969  subrginv  13970  subrgdv  13971  lsselg  14094  islss3  14112  lspsnel3  14138  lsspropdg  14164  rnglidlmcl  14213  znf1o  14384  topssnei  14605  cnprcl2k  14649  cnss1  14669  cnptopresti  14681  cnptoprest  14682  lmres  14691  txopn  14708  txcnp  14714  xmetres2  14822  blin2  14875  blopn  14933  xmettxlem  14952  xmettx  14953  elcncf2  15017  cncfmet  15035  cncfmptc  15039  cncfmptid  15040  negcncf  15048  mulcncflem  15050  cnrehmeocntop  15053  dedekindeulemuub  15060  dedekindeulemlu  15064  suplociccreex  15067  suplociccex  15068  dedekindicclemuub  15069  dedekindicclemlu  15073  dedekindicclemeu  15074  dedekindicclemicc  15075  ivthinclemlopn  15079  ivthinclemuopn  15081  ivthdec  15087  limcimolemlt  15107  cnplimcim  15110  cnplimclemle  15111  cnplimclemr  15112  cnlimci  15116  limccnpcntop  15118  limccnp2lem  15119  limccnp2cntop  15120  dvlemap  15123  dvfgg  15131  dvidsslem  15136  dvconstss  15141  dvcnp2cntop  15142  dvaddxxbr  15144  dvmulxxbr  15145  dvcoapbr  15150  dvcjbr  15151  plyf  15180  plycolemc  15201  dvply2g  15209  reeff1olem  15214  lgsquadlem3  15527  sssneq  15901