Theorem sselda 3248

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 3247	. 2 |- ( ph -> ( C e. A -> C e. B ) )
3	2	imp 124	1 |- ( ( ph /\ C e. A ) -> C e. B )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   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:  pwntru  4336  elrel  4877  ffvresb  5871  1stdm  6416  tfrlem1  6579  tfrlemiubacc  6601  tfr1onlemubacc  6617  tfrcllemubacc  6630  erinxp  6883  fundmen  7094  supisolem  7348  ordiso2  7375  difinfsn  7440  ctssdc  7453  exmidfodomrlemeldju  7551  exmidfodomrlemreseldju  7552  pw1m  7583  pw1on  7585  elprnql  7848  elprnqu  7849  suplocexprlemml  8083  axpre-suploclemres  8268  suprleubex  9284  un0addcl  9596  un0mulcl  9597  suprzclex  9744  supminfex  9997  infregelbex  9998  icoshftf1o  10393  elfzom1elfzo  10621  zpnn0elfzo  10625  seqfveqg  10915  seq3fveq  10916  monoord2  10923  seqsplitg  10926  seqcaopr2g  10931  seqf1oglem2a  10955  seqf1oglem2  10957  seqhomog  10967  seq3coll  11294  ccatass  11376  ccatrn  11377  ccatalpha  11381  pfxf  11454  swrdccatin2  11501  pfxccatin12lem2c  11502  rexanre  11986  rexico  11987  summodclem2a  12148  isumss  12158  fisumss  12159  fsum3cvg3  12163  fsumsplit  12174  fsum2dlemstep  12201  fisum0diag2  12214  fsumlessfi  12227  fsumabs  12232  telfsumo  12233  fsumparts  12237  fsumrelem  12238  fsumiun  12244  hashuni  12249  binom1dif  12254  isumsplit  12258  isumrpcl  12261  isumlessdc  12263  mertenslemi1  12302  clim2prod  12306  prodfrecap  12313  prodmodclem2a  12343  prodssdc  12356  fprodssdc  12357  fprodsplitdc  12363  fprod2dlemstep  12389  4sqlemffi  13175  4sqleminfi  13176  4sqlem11  13180  ballotfilemsel1i  13256  ballotfilemsima  13259  ballotfilemfrceq  13272  ennnfonelemfun  13308  ennnfonelemf1  13309  restid2  13602  gzsumress  13712  gzsumsplit1r  13715  issubmnd  13755  ress0g  13756  grpinvssd  13882  subginv  13984  issubg2m  13992  issubg4m  13996  subgintm  14001  ssnmz  14014  resghm  14063  conjnmz  14082  conjnmzb  14083  subcmnd  14137  gsummptfidmadd  14161  ringidss  14334  invrpropdg  14456  subrg1  14539  subrginv  14545  subrgunit  14547  islss3  14716  lssintclm  14721  issubassa2  15035  tgclb  15166  tgidm  15175  tgrest  15270  txcnp  15372  txdis1cn  15379  psmetres2  15434  blpnfctr  15540  xmetresbl  15541  mopni2  15584  mopni3  15585  rnblopn  15590  xmettx  15611  tgioo  15655  fsumcncntop  15668  climcncf  15685  suplociccreex  15725  suplociccex  15726  dedekindicc  15734  ivthdec  15745  dvfgg  15789  dvcnp2cntop  15800  dvaddxxbr  15802  dvcjbr  15809  dvmptfsum  15826  perfectlem2  16114  gausslemma2dlem2  16181  gausslemma2dlem3  16182  lgsquadlem2  16197  uhgredgm  16377  edgumgren  16383  edgusgren  16404  wlkres  16620  clwwlkccatlem  16641  pwtrufal  17027