Theorem sseld 3123

Description: Membership deduction from subclass relationship. (Contributed by NM, 15-Nov-1995.)

Hypothesis

Ref	Expression
sseld.1	|- ( ph -> A C_ B )

Assertion

Ref	Expression
sseld	|- ( ph -> ( C e. A -> C e. B ) )

Proof of Theorem sseld

Step	Hyp	Ref	Expression
1		sseld.1	. 2 |- ( ph -> A C_ B )
2		ssel 3118	. 2 |- ( A C_ B -> ( C e. A -> C e. B ) )
3	1, 2	syl 14	1 |- ( ph -> ( C e. A -> C e. B ) )

Syntax hints:   -> wi 4   e. wcel 2125   C_ wss 3098

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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-11 1483  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-ext 2136

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1740  df-clab 2141  df-cleq 2147  df-clel 2150  df-in 3104  df-ss 3111

This theorem is referenced by:  sselda  3124  sseldd  3125  ssneld  3126  elelpwi  3551  ssbrd  4003  uniopel  4211  onintonm  4470  sucprcreg  4502  ordsuc  4516  0elnn  4572  dmrnssfld  4842  nfunv  5196  opelf  5334  fvimacnv  5575  ffvelrn  5593  resflem  5624  f1imass  5715  dftpos3  6199  nnmordi  6452  mapsn  6624  ixpf  6654  diffifi  6828  ordiso2  6965  difinfinf  7031  prarloclemarch2  7318  ltexprlemrl  7509  cauappcvgprlemladdrl  7556  caucvgprlemladdrl  7577  caucvgprlem1  7578  axpre-suploclemres  7800  uzind  9254  supinfneg  9485  infsupneg  9486  ixxssxr  9782  elfz0add  10000  fzoss1  10048  frecuzrdgrclt  10292  fsum3cvg  11252  isumrpcl  11368  fproddccvg  11446  lmtopcnp  12589  txuni2  12595  tx1cn  12608  tx2cn  12609  txlm  12618  imasnopn  12638  xmetunirn  12697  mopnval  12781  metrest  12845  dedekindicc  12950  ivthdec  12961  limcimolemlt  12972  bj-charfundc  13321  bj-nnord  13471