Theorem sselda 3201

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 3200	. 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 2178   C_ wss 3174

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-in 3180  df-ss 3187

This theorem is referenced by:  pwntru  4259  elrel  4795  ffvresb  5766  1stdm  6291  tfrlem1  6417  tfrlemiubacc  6439  tfr1onlemubacc  6455  tfrcllemubacc  6468  erinxp  6719  fundmen  6922  supisolem  7136  ordiso2  7163  difinfsn  7228  ctssdc  7241  exmidfodomrlemeldju  7338  exmidfodomrlemreseldju  7339  pw1m  7370  pw1on  7372  elprnql  7629  elprnqu  7630  suplocexprlemml  7864  axpre-suploclemres  8049  suprleubex  9062  un0addcl  9363  un0mulcl  9364  suprzclex  9506  supminfex  9753  infregelbex  9754  icoshftf1o  10148  elfzom1elfzo  10369  zpnn0elfzo  10373  seqfveqg  10660  seq3fveq  10661  monoord2  10668  seqsplitg  10671  seqcaopr2g  10676  seqf1oglem2a  10700  seqf1oglem2  10702  seqhomog  10712  seq3coll  11024  ccatass  11102  ccatrn  11103  pfxf  11173  swrdccatin2  11220  pfxccatin12lem2c  11221  rexanre  11646  rexico  11647  summodclem2a  11807  isumss  11817  fisumss  11818  fsum3cvg3  11822  fsumsplit  11833  fsum2dlemstep  11860  fisum0diag2  11873  fsumlessfi  11886  fsumabs  11891  telfsumo  11892  fsumparts  11896  fsumrelem  11897  fsumiun  11903  hashuni  11908  binom1dif  11913  isumsplit  11917  isumrpcl  11920  isumlessdc  11922  mertenslemi1  11961  clim2prod  11965  prodfrecap  11972  prodmodclem2a  12002  prodssdc  12015  fprodssdc  12016  fprodsplitdc  12022  fprod2dlemstep  12048  4sqlemffi  12834  4sqleminfi  12835  4sqlem11  12839  ennnfonelemfun  12903  ennnfonelemf1  12904  restid2  13195  gsumress  13342  gsumsplit1r  13345  issubmnd  13389  ress0g  13390  grpinvssd  13524  subginv  13632  issubg2m  13640  issubg4m  13644  subgintm  13649  ssnmz  13662  resghm  13711  conjnmz  13730  conjnmzb  13731  subcmnd  13784  ringidss  13906  invrpropdg  14026  subrg1  14108  subrginv  14114  subrgunit  14116  islss3  14256  lssintclm  14261  tgclb  14652  tgidm  14661  tgrest  14756  txcnp  14858  txdis1cn  14865  psmetres2  14920  blpnfctr  15026  xmetresbl  15027  mopni2  15070  mopni3  15071  rnblopn  15076  xmettx  15097  tgioo  15141  fsumcncntop  15154  climcncf  15171  suplociccreex  15211  suplociccex  15212  dedekindicc  15220  ivthdec  15231  dvfgg  15275  dvcnp2cntop  15286  dvaddxxbr  15288  dvcjbr  15295  dvmptfsum  15312  perfectlem2  15587  gausslemma2dlem2  15654  gausslemma2dlem3  15655  lgsquadlem2  15670  uhgredgm  15842  edgumgren  15846  pwtrufal  16136