Theorem sselda 3238

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 3237	. 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 2203   C_ wss 3211

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 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3217  df-ss 3224

This theorem is referenced by:  pwntru  4312  elrel  4852  ffvresb  5840  1stdm  6376  tfrlem1  6539  tfrlemiubacc  6561  tfr1onlemubacc  6577  tfrcllemubacc  6590  erinxp  6843  fundmen  7047  supisolem  7299  ordiso2  7326  difinfsn  7391  ctssdc  7404  exmidfodomrlemeldju  7502  exmidfodomrlemreseldju  7503  pw1m  7534  pw1on  7536  elprnql  7796  elprnqu  7797  suplocexprlemml  8031  axpre-suploclemres  8216  suprleubex  9228  un0addcl  9529  un0mulcl  9530  suprzclex  9676  supminfex  9929  infregelbex  9930  icoshftf1o  10324  elfzom1elfzo  10548  zpnn0elfzo  10552  seqfveqg  10840  seq3fveq  10841  monoord2  10848  seqsplitg  10851  seqcaopr2g  10856  seqf1oglem2a  10880  seqf1oglem2  10882  seqhomog  10892  seq3coll  11214  ccatass  11296  ccatrn  11297  ccatalpha  11301  pfxf  11374  swrdccatin2  11421  pfxccatin12lem2c  11422  rexanre  11905  rexico  11906  summodclem2a  12067  isumss  12077  fisumss  12078  fsum3cvg3  12082  fsumsplit  12093  fsum2dlemstep  12120  fisum0diag2  12133  fsumlessfi  12146  fsumabs  12151  telfsumo  12152  fsumparts  12156  fsumrelem  12157  fsumiun  12163  hashuni  12168  binom1dif  12173  isumsplit  12177  isumrpcl  12180  isumlessdc  12182  mertenslemi1  12221  clim2prod  12225  prodfrecap  12232  prodmodclem2a  12262  prodssdc  12275  fprodssdc  12276  fprodsplitdc  12282  fprod2dlemstep  12308  4sqlemffi  13094  4sqleminfi  13095  4sqlem11  13099  ennnfonelemfun  13168  ennnfonelemf1  13169  restid2  13461  gsumress  13608  gsumsplit1r  13611  issubmnd  13655  ress0g  13656  grpinvssd  13790  subginv  13898  issubg2m  13906  issubg4m  13910  subgintm  13915  ssnmz  13928  resghm  13977  conjnmz  13996  conjnmzb  13997  subcmnd  14050  ringidss  14173  invrpropdg  14294  subrg1  14376  subrginv  14382  subrgunit  14384  islss3  14527  lssintclm  14532  tgclb  14930  tgidm  14939  tgrest  15034  txcnp  15136  txdis1cn  15143  psmetres2  15198  blpnfctr  15304  xmetresbl  15305  mopni2  15348  mopni3  15349  rnblopn  15354  xmettx  15375  tgioo  15419  fsumcncntop  15432  climcncf  15449  suplociccreex  15489  suplociccex  15490  dedekindicc  15498  ivthdec  15509  dvfgg  15553  dvcnp2cntop  15564  dvaddxxbr  15566  dvcjbr  15573  dvmptfsum  15590  perfectlem2  15868  gausslemma2dlem2  15935  gausslemma2dlem3  15936  lgsquadlem2  15951  uhgredgm  16131  edgumgren  16137  edgusgren  16158  wlkres  16374  clwwlkccatlem  16395  pwtrufal  16771