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  9286  un0addcl  9600  un0mulcl  9601  suprzclex  9748  supminfex  10006  infregelbex  10007  icoshftf1o  10403  elfzom1elfzo  10631  zpnn0elfzo  10635  seqfveqg  10928  seq3fveq  10929  monoord2  10936  seqsplitg  10939  seqcaopr2g  10944  seqf1oglem2a  10968  seqf1oglem2  10970  seqhomog  10980  seq3coll  11308  ccatass  11390  ccatrn  11391  ccatalpha  11395  pfxf  11468  swrdccatin2  11515  pfxccatin12lem2c  11516  rexanre  12001  rexico  12002  summodclem2a  12164  isumss  12174  fisumss  12175  fsum3cvg3  12179  fsumsplit  12190  fsum2dlemstep  12217  fisum0diag2  12230  fsumlessfi  12243  fsumabs  12248  telfsumo  12249  fsumparts  12253  fsumrelem  12254  fsumiun  12260  hashuni  12265  binom1dif  12270  isumsplit  12274  isumrpcl  12277  isumlessdc  12279  mertenslemi1  12318  clim2prod  12322  prodfrecap  12329  prodmodclem2a  12359  prodssdc  12372  fprodssdc  12373  fprodsplitdc  12379  fprod2dlemstep  12405  4sqlemffi  13195  4sqleminfi  13196  4sqlem11  13200  ballotfilemsel1i  13305  ballotfilemsima  13308  ballotfilemfrceq  13321  ennnfonelemfun  13357  ennnfonelemf1  13358  restid2  13651  gzsumress  13761  gzsumsplit1r  13764  issubmnd  13804  ress0g  13805  grpinvssd  13931  subginv  14033  issubg2m  14041  issubg4m  14045  subgintm  14050  ssnmz  14063  resghm  14112  conjnmz  14131  conjnmzb  14132  subcmnd  14186  gsummptfidmadd  14210  ringidss  14383  invrpropdg  14505  subrg1  14588  subrginv  14594  subrgunit  14596  islss3  14765  lssintclm  14770  issubassa2  15084  tgclb  15215  tgidm  15224  tgrest  15319  txcnp  15421  txdis1cn  15428  psmetres2  15483  blpnfctr  15589  xmetresbl  15590  mopni2  15633  mopni3  15634  rnblopn  15639  xmettx  15660  tgioo  15704  fsumcncntop  15717  climcncf  15734  suplociccreex  15774  suplociccex  15775  dedekindicc  15783  ivthdec  15794  dvfgg  15838  dvcnp2cntop  15849  dvaddxxbr  15851  dvcjbr  15858  dvmptfsum  15875  perfectlem2  16198  gausslemma2dlem2  16279  gausslemma2dlem3  16280  lgsquadlem2  16295  uhgredgm  16475  edgumgren  16481  edgusgren  16502  wlkres  16718  clwwlkccatlem  16739  pwtrufal  17125