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  4338  elrel  4879  ffvresb  5874  1stdm  6420  tfrlem1  6584  tfrlemiubacc  6606  tfr1onlemubacc  6622  tfrcllemubacc  6635  erinxp  6888  fundmen  7100  funisfsuppdc  7298  supisolem  7354  ordiso2  7381  difinfsn  7446  ctssdc  7459  exmidfodomrlemeldju  7557  exmidfodomrlemreseldju  7558  pw1m  7589  pw1on  7591  elprnql  7854  elprnqu  7855  suplocexprlemml  8089  axpre-suploclemres  8274  suprleubex  9292  un0addcl  9607  un0mulcl  9608  suprzclex  9754  supminfex  10012  infregelbex  10013  icoshftf1o  10409  elfzom1elfzo  10637  zpnn0elfzo  10641  seqfveqg  10935  seq3fveq  10936  monoord2  10943  seqsplitg  10946  seqcaopr2g  10951  seqf1oglem2a  10975  seqf1oglem2  10977  seqhomog  10987  seq3coll  11315  ccatass  11397  ccatrn  11398  ccatalpha  11402  pfxf  11475  swrdccatin2  11522  pfxccatin12lem2c  11523  rexanre  12008  rexico  12009  summodclem2a  12172  isumss  12182  fisumss  12183  fsum3cvg3  12187  fsumsplit  12198  fsum2dlemstep  12225  fisum0diag2  12238  fsumlessfi  12251  fsumabs  12256  telfsumo  12257  fsumparts  12261  fsumrelem  12262  fsumiun  12268  hashuni  12273  binom1dif  12278  isumsplit  12282  isumrpcl  12285  isumlessdc  12287  mertenslemi1  12326  clim2prod  12330  prodfrecap  12337  prodmodclem2a  12367  prodssdc  12380  fprodssdc  12381  fprodsplitdc  12387  fprod2dlemstep  12413  4sqlemffi  13203  4sqleminfi  13204  4sqlem11  13208  ballotfilemsel1i  13313  ballotfilemsima  13316  ballotfilemfrceq  13329  ennnfonelemfun  13365  ennnfonelemf1  13366  restid2  13660  gzsumress  13770  gzsumsplit1r  13773  issubmnd  13813  ress0g  13814  grpinvssd  13940  subginv  14042  issubg2m  14050  issubg4m  14054  subgintm  14059  ssnmz  14072  resghm  14121  conjnmz  14140  conjnmzb  14141  cntzsgrpcl  14166  cntzsubm  14169  cntzmhm  14172  subcmnd  14226  gsummptfidmadd  14250  gsummptfidmsplit  14253  gsumresfi  14262  gsum2dfilem2  14271  ringidss  14440  invrpropdg  14564  subrg1  14647  subrginv  14653  subrgunit  14655  islss3  14824  lssintclm  14829  issubassa2  15143  psrbaglefifi  15175  psrbagmaxlem1x  15181  psrbagmaxlem1y  15182  tgclb  15308  tgidm  15317  tgrest  15412  txcnp  15514  txdis1cn  15521  psmetres2  15576  blpnfctr  15682  xmetresbl  15683  mopni2  15726  mopni3  15727  rnblopn  15732  xmettx  15753  tgioo  15797  fsumcncntop  15810  climcncf  15827  suplociccreex  15867  suplociccex  15868  dedekindicc  15876  ivthdec  15887  dvfgg  15931  dvcnp2cntop  15942  dvaddxxbr  15944  dvcjbr  15951  dvmptfsum  15968  chtdif  16281  chtublem  16312  perfectlem2  16317  gausslemma2dlem2  16403  gausslemma2dlem3  16404  lgsquadlem2  16419  uhgredgm  16599  edgumgren  16605  edgusgren  16626  wlkres  16842  clwwlkccatlem  16863  pwtrufal  17249