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 )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2209   C_ wss 3220

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 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 theorem 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 referenced by:  pwntru  4331  elrel  4872  ffvresb  5862  1stdm  6406  tfrlem1  6569  tfrlemiubacc  6591  tfr1onlemubacc  6607  tfrcllemubacc  6620  erinxp  6873  fundmen  7084  supisolem  7338  ordiso2  7365  difinfsn  7430  ctssdc  7443  exmidfodomrlemeldju  7541  exmidfodomrlemreseldju  7542  pw1m  7573  pw1on  7575  elprnql  7838  elprnqu  7839  suplocexprlemml  8073  axpre-suploclemres  8258  suprleubex  9274  un0addcl  9575  un0mulcl  9576  suprzclex  9723  supminfex  9976  infregelbex  9977  icoshftf1o  10372  elfzom1elfzo  10599  zpnn0elfzo  10603  seqfveqg  10893  seq3fveq  10894  monoord2  10901  seqsplitg  10904  seqcaopr2g  10909  seqf1oglem2a  10933  seqf1oglem2  10935  seqhomog  10945  seq3coll  11272  ccatass  11354  ccatrn  11355  ccatalpha  11359  pfxf  11432  swrdccatin2  11479  pfxccatin12lem2c  11480  rexanre  11964  rexico  11965  summodclem2a  12126  isumss  12136  fisumss  12137  fsum3cvg3  12141  fsumsplit  12152  fsum2dlemstep  12179  fisum0diag2  12192  fsumlessfi  12205  fsumabs  12210  telfsumo  12211  fsumparts  12215  fsumrelem  12216  fsumiun  12222  hashuni  12227  binom1dif  12232  isumsplit  12236  isumrpcl  12239  isumlessdc  12241  mertenslemi1  12280  clim2prod  12284  prodfrecap  12291  prodmodclem2a  12321  prodssdc  12334  fprodssdc  12335  fprodsplitdc  12341  fprod2dlemstep  12367  4sqlemffi  13153  4sqleminfi  13154  4sqlem11  13158  ballotfilemsel1i  13234  ballotfilemsima  13237  ballotfilemfrceq  13250  ennnfonelemfun  13286  ennnfonelemf1  13287  restid2  13579  gzsumress  13689  gzsumsplit1r  13692  issubmnd  13732  ress0g  13733  grpinvssd  13859  subginv  13961  issubg2m  13969  issubg4m  13973  subgintm  13978  ssnmz  13991  resghm  14040  conjnmz  14059  conjnmzb  14060  subcmnd  14114  gsummptfidmadd  14138  ringidss  14307  invrpropdg  14429  subrg1  14512  subrginv  14518  subrgunit  14520  islss3  14688  lssintclm  14693  tgclb  15089  tgidm  15098  tgrest  15193  txcnp  15295  txdis1cn  15302  psmetres2  15357  blpnfctr  15463  xmetresbl  15464  mopni2  15507  mopni3  15508  rnblopn  15513  xmettx  15534  tgioo  15578  fsumcncntop  15591  climcncf  15608  suplociccreex  15648  suplociccex  15649  dedekindicc  15657  ivthdec  15668  dvfgg  15712  dvcnp2cntop  15723  dvaddxxbr  15725  dvcjbr  15732  dvmptfsum  15749  perfectlem2  16028  gausslemma2dlem2  16095  gausslemma2dlem3  16096  lgsquadlem2  16111  uhgredgm  16291  edgumgren  16297  edgusgren  16318  wlkres  16534  clwwlkccatlem  16555  pwtrufal  16941