Theorem sselda 3142

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 3141	. 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 2136   C_ wss 3116

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-11 1494  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-in 3122  df-ss 3129

This theorem is referenced by:  pwntru  4178  elrel  4706  ffvresb  5648  1stdm  6150  tfrlem1  6276  tfrlemiubacc  6298  tfr1onlemubacc  6314  tfrcllemubacc  6327  erinxp  6575  fundmen  6772  supisolem  6973  ordiso2  7000  difinfsn  7065  ctssdc  7078  exmidfodomrlemeldju  7155  exmidfodomrlemreseldju  7156  pw1on  7182  elprnql  7422  elprnqu  7423  suplocexprlemml  7657  axpre-suploclemres  7842  suprleubex  8849  un0addcl  9147  un0mulcl  9148  suprzclex  9289  supminfex  9535  infregelbex  9536  icoshftf1o  9927  elfzom1elfzo  10138  zpnn0elfzo  10142  seq3fveq  10406  monoord2  10412  seq3coll  10755  rexanre  11162  rexico  11163  summodclem2a  11322  isumss  11332  fisumss  11333  fsum3cvg3  11337  fsumsplit  11348  fsum2dlemstep  11375  fisum0diag2  11388  fsumlessfi  11401  fsumabs  11406  telfsumo  11407  fsumparts  11411  fsumrelem  11412  fsumiun  11418  hashuni  11423  binom1dif  11428  isumsplit  11432  isumrpcl  11435  isumlessdc  11437  mertenslemi1  11476  clim2prod  11480  prodfrecap  11487  prodmodclem2a  11517  prodssdc  11530  fprodssdc  11531  fprodsplitdc  11537  fprod2dlemstep  11563  ennnfonelemfun  12350  ennnfonelemf1  12351  restid2  12565  tgclb  12705  tgidm  12714  tgrest  12809  txcnp  12911  txdis1cn  12918  psmetres2  12973  blpnfctr  13079  xmetresbl  13080  mopni2  13123  mopni3  13124  rnblopn  13129  xmettx  13150  tgioo  13186  fsumcncntop  13196  climcncf  13211  suplociccreex  13242  suplociccex  13243  dedekindicc  13251  ivthdec  13262  dvfgg  13297  dvcnp2cntop  13303  dvaddxxbr  13305  dvcjbr  13312  pwtrufal  13877