Theorem sseld 3227

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 3222	. 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 2202   C_ wss 3201

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 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  sselda  3228  sseldd  3229  ssneld  3230  elelpwi  3668  ssbrd  4136  uniopel  4355  onintonm  4621  sucprcreg  4653  ordsuc  4667  0elnn  4723  dmrnssfld  5001  nfunv  5366  opelf  5515  fvimacnv  5771  ffvelcdm  5788  resflem  5819  f1imass  5925  suppssrst  6439  suppssrgst  6440  dftpos3  6471  nnmordi  6727  mapsn  6902  ixpf  6932  pw2f1odclem  7063  diffifi  7126  ordiso2  7294  difinfinf  7360  exmidapne  7539  prarloclemarch2  7699  ltexprlemrl  7890  cauappcvgprlemladdrl  7937  caucvgprlemladdrl  7958  caucvgprlem1  7959  axpre-suploclemres  8181  uzind  9652  supinfneg  9890  infsupneg  9891  ixxssxr  10196  elfz0add  10417  fzoss1  10470  elfzoextl  10499  frecuzrdgrclt  10740  ccatval2  11241  swrdswrd  11352  pfxccatin12lem2a  11374  swrdccatin2  11376  pfxccatpfx2  11384  fsum3cvg  12019  isumrpcl  12135  fproddccvg  12213  reumodprminv  12906  issubmnd  13605  issubg2m  13856  eqgid  13893  issubrng2  14305  subrgdvds  14330  issubrg2  14336  lssats2  14510  rnglidlmmgm  14592  rnglidlmsgrp  14593  rnglidlrng  14594  mplbasss  14797  lmtopcnp  15061  txuni2  15067  tx1cn  15080  tx2cn  15081  txlm  15090  imasnopn  15110  xmetunirn  15169  mopnval  15253  metrest  15317  dedekindicc  15444  ivthdec  15455  limcimolemlt  15475  plyssc  15550  edgupgren  16082  subgreldmiedg  16210  clwwlkccatlem  16341  eupth2lemsfi  16419  bj-charfundc  16524  bj-nnord  16674