Theorem sseld 3101

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 3096	. 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 1481   C_ wss 3076

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 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-in 3082  df-ss 3089

This theorem is referenced by:  sselda  3102  sseldd  3103  ssneld  3104  elelpwi  3527  ssbrd  3979  uniopel  4186  onintonm  4441  sucprcreg  4472  ordsuc  4486  0elnn  4540  dmrnssfld  4810  nfunv  5164  opelf  5302  fvimacnv  5543  ffvelrn  5561  resflem  5592  f1imass  5683  dftpos3  6167  nnmordi  6420  mapsn  6592  ixpf  6622  diffifi  6796  ordiso2  6928  difinfinf  6994  prarloclemarch2  7251  ltexprlemrl  7442  cauappcvgprlemladdrl  7489  caucvgprlemladdrl  7510  caucvgprlem1  7511  axpre-suploclemres  7733  uzind  9186  supinfneg  9417  infsupneg  9418  ixxssxr  9713  elfz0add  9931  fzoss1  9979  frecuzrdgrclt  10219  fsum3cvg  11179  isumrpcl  11295  fproddccvg  11373  lmtopcnp  12458  txuni2  12464  tx1cn  12477  tx2cn  12478  txlm  12487  imasnopn  12507  xmetunirn  12566  mopnval  12650  metrest  12714  dedekindicc  12819  ivthdec  12830  limcimolemlt  12841  bj-nnord  13327