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  7349  ordiso2  7376  difinfsn  7441  ctssdc  7454  exmidfodomrlemeldju  7552  exmidfodomrlemreseldju  7553  pw1m  7584  pw1on  7586  elprnql  7849  elprnqu  7850  suplocexprlemml  8084  axpre-suploclemres  8269  suprleubex  9287  un0addcl  9601  un0mulcl  9602  suprzclex  9749  supminfex  10007  infregelbex  10008  icoshftf1o  10404  elfzom1elfzo  10632  zpnn0elfzo  10636  seqfveqg  10930  seq3fveq  10931  monoord2  10938  seqsplitg  10941  seqcaopr2g  10946  seqf1oglem2a  10970  seqf1oglem2  10972  seqhomog  10982  seq3coll  11310  ccatass  11392  ccatrn  11393  ccatalpha  11397  pfxf  11470  swrdccatin2  11517  pfxccatin12lem2c  11518  rexanre  12003  rexico  12004  summodclem2a  12167  isumss  12177  fisumss  12178  fsum3cvg3  12182  fsumsplit  12193  fsum2dlemstep  12220  fisum0diag2  12233  fsumlessfi  12246  fsumabs  12251  telfsumo  12252  fsumparts  12256  fsumrelem  12257  fsumiun  12263  hashuni  12268  binom1dif  12273  isumsplit  12277  isumrpcl  12280  isumlessdc  12282  mertenslemi1  12321  clim2prod  12325  prodfrecap  12332  prodmodclem2a  12362  prodssdc  12375  fprodssdc  12376  fprodsplitdc  12382  fprod2dlemstep  12408  4sqlemffi  13198  4sqleminfi  13199  4sqlem11  13203  ballotfilemsel1i  13308  ballotfilemsima  13311  ballotfilemfrceq  13324  ennnfonelemfun  13360  ennnfonelemf1  13361  restid2  13655  gzsumress  13765  gzsumsplit1r  13768  issubmnd  13808  ress0g  13809  grpinvssd  13935  subginv  14037  issubg2m  14045  issubg4m  14049  subgintm  14054  ssnmz  14067  resghm  14116  conjnmz  14135  conjnmzb  14136  cntzsgrpcl  14161  cntzsubm  14164  cntzmhm  14167  subcmnd  14221  gsummptfidmadd  14245  ringidss  14418  invrpropdg  14540  subrg1  14623  subrginv  14629  subrgunit  14631  islss3  14800  lssintclm  14805  issubassa2  15119  psrbaglefifi  15147  tgclb  15257  tgidm  15266  tgrest  15361  txcnp  15463  txdis1cn  15470  psmetres2  15525  blpnfctr  15631  xmetresbl  15632  mopni2  15675  mopni3  15676  rnblopn  15681  xmettx  15702  tgioo  15746  fsumcncntop  15759  climcncf  15776  suplociccreex  15816  suplociccex  15817  dedekindicc  15825  ivthdec  15836  dvfgg  15880  dvcnp2cntop  15891  dvaddxxbr  15893  dvcjbr  15900  dvmptfsum  15917  chtdif  16225  chtublem  16256  perfectlem2  16261  gausslemma2dlem2  16347  gausslemma2dlem3  16348  lgsquadlem2  16363  uhgredgm  16543  edgumgren  16549  edgusgren  16570  wlkres  16786  clwwlkccatlem  16807  pwtrufal  17193