Theorem sseld 3239

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 3234	. 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 2205   C_ wss 3213

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3219  df-ss 3226

This theorem is referenced by:  sselda  3240  sseldd  3241  ssneld  3242  elelpwi  3683  ssbrd  4154  uniopel  4375  onintonm  4641  sucprcreg  4673  ordsuc  4687  0elnn  4743  dmrnssfld  5022  nfunv  5387  opelf  5537  fvimacnv  5795  ffvelcdm  5812  resflem  5843  f1imass  5949  suppssrst  6463  suppssrgst  6464  dftpos3  6495  nnmordi  6751  mapsnd  6925  mapsn  6927  ixpf  6957  pw2f1odclem  7089  diffifi  7153  ordiso2  7328  difinfinf  7394  exmidapne  7576  prarloclemarch2  7736  ltexprlemrl  7927  cauappcvgprlemladdrl  7974  caucvgprlemladdrl  7995  caucvgprlem1  7996  axpre-suploclemres  8218  uzind  9692  supinfneg  9930  infsupneg  9931  ixxssxr  10236  elfz0add  10458  fzoss1  10511  elfzoextl  10540  frecuzrdgrclt  10781  ccatval2  11290  swrdswrd  11401  pfxccatin12lem2a  11423  swrdccatin2  11425  pfxccatpfx2  11433  fsum3cvg  12068  isumrpcl  12184  fproddccvg  12262  reumodprminv  12955  ballotfilemfc0  13153  ballotfilemfcc  13154  issubmnd  13672  issubg2m  13923  eqgid  13960  issubrng2  14372  subrgdvds  14397  issubrg2  14403  lssats2  14579  rnglidlmmgm  14661  rnglidlmsgrp  14662  rnglidlrng  14663  mplbasss  14868  lmtopcnp  15132  txuni2  15138  tx1cn  15151  tx2cn  15152  txlm  15161  imasnopn  15181  xmetunirn  15240  mopnval  15324  metrest  15388  dedekindicc  15515  ivthdec  15526  limcimolemlt  15546  plyssc  15621  edgupgren  16153  subgreldmiedg  16281  clwwlkccatlem  16412  eupth2lemsfi  16490  bj-charfundc  16595  bj-nnord  16745