Theorem sselda 3193

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 3192	. 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 2176   C_ wss 3166

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179

This theorem is referenced by:  pwntru  4244  elrel  4778  ffvresb  5745  1stdm  6270  tfrlem1  6396  tfrlemiubacc  6418  tfr1onlemubacc  6434  tfrcllemubacc  6447  erinxp  6698  fundmen  6900  supisolem  7112  ordiso2  7139  difinfsn  7204  ctssdc  7217  exmidfodomrlemeldju  7309  exmidfodomrlemreseldju  7310  pw1on  7340  elprnql  7596  elprnqu  7597  suplocexprlemml  7831  axpre-suploclemres  8016  suprleubex  9029  un0addcl  9330  un0mulcl  9331  suprzclex  9473  supminfex  9720  infregelbex  9721  icoshftf1o  10115  elfzom1elfzo  10334  zpnn0elfzo  10338  seqfveqg  10625  seq3fveq  10626  monoord2  10633  seqsplitg  10636  seqcaopr2g  10641  seqf1oglem2a  10665  seqf1oglem2  10667  seqhomog  10677  seq3coll  10989  ccatass  11067  ccatrn  11068  pfxf  11136  rexanre  11564  rexico  11565  summodclem2a  11725  isumss  11735  fisumss  11736  fsum3cvg3  11740  fsumsplit  11751  fsum2dlemstep  11778  fisum0diag2  11791  fsumlessfi  11804  fsumabs  11809  telfsumo  11810  fsumparts  11814  fsumrelem  11815  fsumiun  11821  hashuni  11826  binom1dif  11831  isumsplit  11835  isumrpcl  11838  isumlessdc  11840  mertenslemi1  11879  clim2prod  11883  prodfrecap  11890  prodmodclem2a  11920  prodssdc  11933  fprodssdc  11934  fprodsplitdc  11940  fprod2dlemstep  11966  4sqlemffi  12752  4sqleminfi  12753  4sqlem11  12757  ennnfonelemfun  12821  ennnfonelemf1  12822  restid2  13113  gsumress  13260  gsumsplit1r  13263  issubmnd  13307  ress0g  13308  grpinvssd  13442  subginv  13550  issubg2m  13558  issubg4m  13562  subgintm  13567  ssnmz  13580  resghm  13629  conjnmz  13648  conjnmzb  13649  subcmnd  13702  ringidss  13824  invrpropdg  13944  subrg1  14026  subrginv  14032  subrgunit  14034  islss3  14174  lssintclm  14179  tgclb  14570  tgidm  14579  tgrest  14674  txcnp  14776  txdis1cn  14783  psmetres2  14838  blpnfctr  14944  xmetresbl  14945  mopni2  14988  mopni3  14989  rnblopn  14994  xmettx  15015  tgioo  15059  fsumcncntop  15072  climcncf  15089  suplociccreex  15129  suplociccex  15130  dedekindicc  15138  ivthdec  15149  dvfgg  15193  dvcnp2cntop  15204  dvaddxxbr  15206  dvcjbr  15213  dvmptfsum  15230  perfectlem2  15505  gausslemma2dlem2  15572  gausslemma2dlem3  15573  lgsquadlem2  15588  pwtrufal  15971