Theorem sselda 3097

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 3096	. 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 3071

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 2121

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-in 3077  df-ss 3084

This theorem is referenced by:  pwntru  4122  elrel  4641  ffvresb  5583  1stdm  6080  tfrlem1  6205  tfrlemiubacc  6227  tfr1onlemubacc  6243  tfrcllemubacc  6256  erinxp  6503  fundmen  6700  supisolem  6895  ordiso2  6920  difinfsn  6985  ctssdc  6998  exmidfodomrlemeldju  7055  exmidfodomrlemreseldju  7056  elprnql  7289  elprnqu  7290  suplocexprlemml  7524  axpre-suploclemres  7709  suprleubex  8712  un0addcl  9010  un0mulcl  9011  suprzclex  9149  supminfex  9392  icoshftf1o  9774  elfzom1elfzo  9980  zpnn0elfzo  9984  seq3fveq  10244  monoord2  10250  seq3coll  10585  rexanre  10992  rexico  10993  summodclem2a  11150  isumss  11160  fisumss  11161  fsum3cvg3  11165  fsumsplit  11176  fsum2dlemstep  11203  fisum0diag2  11216  fsumlessfi  11229  fsumabs  11234  telfsumo  11235  fsumparts  11239  fsumrelem  11240  fsumiun  11246  hashuni  11251  binom1dif  11256  isumsplit  11260  isumrpcl  11263  isumlessdc  11265  mertenslemi1  11304  clim2prod  11308  prodfrecap  11315  prodmodclem2a  11345  ennnfonelemfun  11930  ennnfonelemf1  11931  restid2  12129  tgclb  12234  tgidm  12243  tgrest  12338  txcnp  12440  txdis1cn  12447  psmetres2  12502  blpnfctr  12608  xmetresbl  12609  mopni2  12652  mopni3  12653  rnblopn  12658  xmettx  12679  tgioo  12715  fsumcncntop  12725  climcncf  12740  suplociccreex  12771  suplociccex  12772  dedekindicc  12780  ivthdec  12791  dvfgg  12826  dvcnp2cntop  12832  dvaddxxbr  12834  dvcjbr  12841  pwtrufal  13192