Theorem sselda 3228

Description: Membership deduction from subclass relationship. (Contributed by NM, 26-Jun-2014.)

Hypothesis

Ref	Expression
sseld.1	|- ( ph -> A C_ B )

Assertion

Ref	Expression
sselda	|- ( ( ph /\ C e. A ) -> C e. B )

Proof of Theorem sselda

Step	Hyp	Ref	Expression
1		sseld.1	. . 3 |- ( ph -> A C_ B )
2	1	sseld 3227	. 2 |- ( ph -> ( C e. A -> C e. B ) )
3	2	imp 124	1 |- ( ( ph /\ C e. A ) -> C e. B )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2202   C_ wss 3201

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  pwntru  4295  elrel  4834  ffvresb  5818  1stdm  6354  tfrlem1  6517  tfrlemiubacc  6539  tfr1onlemubacc  6555  tfrcllemubacc  6568  erinxp  6821  fundmen  7024  supisolem  7267  ordiso2  7294  difinfsn  7359  ctssdc  7372  exmidfodomrlemeldju  7470  exmidfodomrlemreseldju  7471  pw1m  7502  pw1on  7504  elprnql  7761  elprnqu  7762  suplocexprlemml  7996  axpre-suploclemres  8181  suprleubex  9193  un0addcl  9494  un0mulcl  9495  suprzclex  9639  supminfex  9892  infregelbex  9893  icoshftf1o  10287  elfzom1elfzo  10511  zpnn0elfzo  10515  seqfveqg  10803  seq3fveq  10804  monoord2  10811  seqsplitg  10814  seqcaopr2g  10819  seqf1oglem2a  10843  seqf1oglem2  10845  seqhomog  10855  seq3coll  11169  ccatass  11251  ccatrn  11252  ccatalpha  11256  pfxf  11329  swrdccatin2  11376  pfxccatin12lem2c  11377  rexanre  11860  rexico  11861  summodclem2a  12022  isumss  12032  fisumss  12033  fsum3cvg3  12037  fsumsplit  12048  fsum2dlemstep  12075  fisum0diag2  12088  fsumlessfi  12101  fsumabs  12106  telfsumo  12107  fsumparts  12111  fsumrelem  12112  fsumiun  12118  hashuni  12123  binom1dif  12128  isumsplit  12132  isumrpcl  12135  isumlessdc  12137  mertenslemi1  12176  clim2prod  12180  prodfrecap  12187  prodmodclem2a  12217  prodssdc  12230  fprodssdc  12231  fprodsplitdc  12237  fprod2dlemstep  12263  4sqlemffi  13049  4sqleminfi  13050  4sqlem11  13054  ennnfonelemfun  13118  ennnfonelemf1  13119  restid2  13411  gsumress  13558  gsumsplit1r  13561  issubmnd  13605  ress0g  13606  grpinvssd  13740  subginv  13848  issubg2m  13856  issubg4m  13860  subgintm  13865  ssnmz  13878  resghm  13927  conjnmz  13946  conjnmzb  13947  subcmnd  14000  ringidss  14123  invrpropdg  14244  subrg1  14326  subrginv  14332  subrgunit  14334  islss3  14475  lssintclm  14480  tgclb  14876  tgidm  14885  tgrest  14980  txcnp  15082  txdis1cn  15089  psmetres2  15144  blpnfctr  15250  xmetresbl  15251  mopni2  15294  mopni3  15295  rnblopn  15300  xmettx  15321  tgioo  15365  fsumcncntop  15378  climcncf  15395  suplociccreex  15435  suplociccex  15436  dedekindicc  15444  ivthdec  15455  dvfgg  15499  dvcnp2cntop  15510  dvaddxxbr  15512  dvcjbr  15519  dvmptfsum  15536  perfectlem2  15814  gausslemma2dlem2  15881  gausslemma2dlem3  15882  lgsquadlem2  15897  uhgredgm  16077  edgumgren  16083  edgusgren  16104  wlkres  16320  clwwlkccatlem  16341  pwtrufal  16719