Theorem sselda 3184

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 3183	. 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 2167   C_ wss 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  pwntru  4233  elrel  4766  ffvresb  5728  1stdm  6249  tfrlem1  6375  tfrlemiubacc  6397  tfr1onlemubacc  6413  tfrcllemubacc  6426  erinxp  6677  fundmen  6874  supisolem  7083  ordiso2  7110  difinfsn  7175  ctssdc  7188  exmidfodomrlemeldju  7278  exmidfodomrlemreseldju  7279  pw1on  7309  elprnql  7565  elprnqu  7566  suplocexprlemml  7800  axpre-suploclemres  7985  suprleubex  8998  un0addcl  9299  un0mulcl  9300  suprzclex  9441  supminfex  9688  infregelbex  9689  icoshftf1o  10083  elfzom1elfzo  10296  zpnn0elfzo  10300  seqfveqg  10587  seq3fveq  10588  monoord2  10595  seqsplitg  10598  seqcaopr2g  10603  seqf1oglem2a  10627  seqf1oglem2  10629  seqhomog  10639  seq3coll  10951  rexanre  11402  rexico  11403  summodclem2a  11563  isumss  11573  fisumss  11574  fsum3cvg3  11578  fsumsplit  11589  fsum2dlemstep  11616  fisum0diag2  11629  fsumlessfi  11642  fsumabs  11647  telfsumo  11648  fsumparts  11652  fsumrelem  11653  fsumiun  11659  hashuni  11664  binom1dif  11669  isumsplit  11673  isumrpcl  11676  isumlessdc  11678  mertenslemi1  11717  clim2prod  11721  prodfrecap  11728  prodmodclem2a  11758  prodssdc  11771  fprodssdc  11772  fprodsplitdc  11778  fprod2dlemstep  11804  4sqlemffi  12590  4sqleminfi  12591  4sqlem11  12595  ennnfonelemfun  12659  ennnfonelemf1  12660  restid2  12950  gsumress  13097  gsumsplit1r  13100  issubmnd  13144  ress0g  13145  grpinvssd  13279  subginv  13387  issubg2m  13395  issubg4m  13399  subgintm  13404  ssnmz  13417  resghm  13466  conjnmz  13485  conjnmzb  13486  subcmnd  13539  ringidss  13661  invrpropdg  13781  subrg1  13863  subrginv  13869  subrgunit  13871  islss3  14011  lssintclm  14016  tgclb  14385  tgidm  14394  tgrest  14489  txcnp  14591  txdis1cn  14598  psmetres2  14653  blpnfctr  14759  xmetresbl  14760  mopni2  14803  mopni3  14804  rnblopn  14809  xmettx  14830  tgioo  14874  fsumcncntop  14887  climcncf  14904  suplociccreex  14944  suplociccex  14945  dedekindicc  14953  ivthdec  14964  dvfgg  15008  dvcnp2cntop  15019  dvaddxxbr  15021  dvcjbr  15028  dvmptfsum  15045  perfectlem2  15320  gausslemma2dlem2  15387  gausslemma2dlem3  15388  lgsquadlem2  15403  pwtrufal  15728