Theorem sselda 3092

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 3091	. 2 |- ( ph -> ( C e. A -> C e. B ) )
3	2	imp 123	1 |- ( ( ph /\ C e. A ) -> C e. B )

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 1480   C_ wss 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-in 3072  df-ss 3079

This theorem is referenced by:  pwntru  4117  elrel  4636  ffvresb  5576  1stdm  6073  tfrlem1  6198  tfrlemiubacc  6220  tfr1onlemubacc  6236  tfrcllemubacc  6249  erinxp  6496  fundmen  6693  supisolem  6888  ordiso2  6913  difinfsn  6978  ctssdc  6991  exmidfodomrlemeldju  7048  exmidfodomrlemreseldju  7049  elprnql  7282  elprnqu  7283  suplocexprlemml  7517  axpre-suploclemres  7702  suprleubex  8705  un0addcl  9003  un0mulcl  9004  suprzclex  9142  supminfex  9385  icoshftf1o  9767  elfzom1elfzo  9973  zpnn0elfzo  9977  seq3fveq  10237  monoord2  10243  seq3coll  10578  rexanre  10985  rexico  10986  summodclem2a  11143  isumss  11153  fisumss  11154  fsum3cvg3  11158  fsumsplit  11169  fsum2dlemstep  11196  fisum0diag2  11209  fsumlessfi  11222  fsumabs  11227  telfsumo  11228  fsumparts  11232  fsumrelem  11233  fsumiun  11239  hashuni  11244  binom1dif  11249  isumsplit  11253  isumrpcl  11256  isumlessdc  11258  mertenslemi1  11297  clim2prod  11301  prodfrecap  11308  ennnfonelemfun  11919  ennnfonelemf1  11920  restid2  12118  tgclb  12223  tgidm  12232  tgrest  12327  txcnp  12429  txdis1cn  12436  psmetres2  12491  blpnfctr  12597  xmetresbl  12598  mopni2  12641  mopni3  12642  rnblopn  12647  xmettx  12668  tgioo  12704  fsumcncntop  12714  climcncf  12729  suplociccreex  12760  suplociccex  12761  dedekindicc  12769  ivthdec  12780  dvfgg  12815  dvcnp2cntop  12821  dvaddxxbr  12823  dvcjbr  12830  pwtrufal  13181