Theorem sseld 3127

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 3122	. 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 2128   C_ wss 3102

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 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-11 1486  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-in 3108  df-ss 3115

This theorem is referenced by:  sselda  3128  sseldd  3129  ssneld  3130  elelpwi  3555  ssbrd  4007  uniopel  4215  onintonm  4474  sucprcreg  4506  ordsuc  4520  0elnn  4576  dmrnssfld  4846  nfunv  5200  opelf  5338  fvimacnv  5579  ffvelrn  5597  resflem  5628  f1imass  5719  dftpos3  6203  nnmordi  6456  mapsn  6628  ixpf  6658  diffifi  6832  ordiso2  6969  difinfinf  7035  prarloclemarch2  7322  ltexprlemrl  7513  cauappcvgprlemladdrl  7560  caucvgprlemladdrl  7581  caucvgprlem1  7582  axpre-suploclemres  7804  uzind  9258  supinfneg  9489  infsupneg  9490  ixxssxr  9786  elfz0add  10004  fzoss1  10052  frecuzrdgrclt  10296  fsum3cvg  11257  isumrpcl  11373  fproddccvg  11451  lmtopcnp  12610  txuni2  12616  tx1cn  12629  tx2cn  12630  txlm  12639  imasnopn  12659  xmetunirn  12718  mopnval  12802  metrest  12866  dedekindicc  12971  ivthdec  12982  limcimolemlt  12993  bj-charfundc  13342  bj-nnord  13492