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  5726  1stdm  6241  tfrlem1  6367  tfrlemiubacc  6389  tfr1onlemubacc  6405  tfrcllemubacc  6418  erinxp  6669  fundmen  6866  supisolem  7075  ordiso2  7102  difinfsn  7167  ctssdc  7180  exmidfodomrlemeldju  7268  exmidfodomrlemreseldju  7269  pw1on  7295  elprnql  7550  elprnqu  7551  suplocexprlemml  7785  axpre-suploclemres  7970  suprleubex  8983  un0addcl  9284  un0mulcl  9285  suprzclex  9426  supminfex  9673  infregelbex  9674  icoshftf1o  10068  elfzom1elfzo  10281  zpnn0elfzo  10285  seqfveqg  10572  seq3fveq  10573  monoord2  10580  seqsplitg  10583  seqcaopr2g  10588  seqf1oglem2a  10612  seqf1oglem2  10614  seqhomog  10624  seq3coll  10936  rexanre  11387  rexico  11388  summodclem2a  11548  isumss  11558  fisumss  11559  fsum3cvg3  11563  fsumsplit  11574  fsum2dlemstep  11601  fisum0diag2  11614  fsumlessfi  11627  fsumabs  11632  telfsumo  11633  fsumparts  11637  fsumrelem  11638  fsumiun  11644  hashuni  11649  binom1dif  11654  isumsplit  11658  isumrpcl  11661  isumlessdc  11663  mertenslemi1  11702  clim2prod  11706  prodfrecap  11713  prodmodclem2a  11743  prodssdc  11756  fprodssdc  11757  fprodsplitdc  11763  fprod2dlemstep  11789  4sqlemffi  12575  4sqleminfi  12576  4sqlem11  12580  ennnfonelemfun  12644  ennnfonelemf1  12645  restid2  12929  gsumress  13048  gsumsplit1r  13051  issubmnd  13093  ress0g  13094  grpinvssd  13219  subginv  13321  issubg2m  13329  issubg4m  13333  subgintm  13338  ssnmz  13351  resghm  13400  conjnmz  13419  conjnmzb  13420  subcmnd  13473  ringidss  13595  invrpropdg  13715  subrg1  13797  subrginv  13803  subrgunit  13805  islss3  13945  lssintclm  13950  tgclb  14311  tgidm  14320  tgrest  14415  txcnp  14517  txdis1cn  14524  psmetres2  14579  blpnfctr  14685  xmetresbl  14686  mopni2  14729  mopni3  14730  rnblopn  14735  xmettx  14756  tgioo  14800  fsumcncntop  14813  climcncf  14830  suplociccreex  14870  suplociccex  14871  dedekindicc  14879  ivthdec  14890  dvfgg  14934  dvcnp2cntop  14945  dvaddxxbr  14947  dvcjbr  14954  dvmptfsum  14971  perfectlem2  15246  gausslemma2dlem2  15313  gausslemma2dlem3  15314  lgsquadlem2  15329  pwtrufal  15652