Theorem sseld 3200

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 3195	. 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 2178   C_ wss 3174

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-in 3180  df-ss 3187

This theorem is referenced by:  sselda  3201  sseldd  3202  ssneld  3203  elelpwi  3638  ssbrd  4102  uniopel  4319  onintonm  4583  sucprcreg  4615  ordsuc  4629  0elnn  4685  dmrnssfld  4960  nfunv  5323  opelf  5468  fvimacnv  5718  ffvelcdm  5736  resflem  5767  f1imass  5866  dftpos3  6371  nnmordi  6625  mapsn  6800  ixpf  6830  pw2f1odclem  6956  diffifi  7017  ordiso2  7163  difinfinf  7229  exmidapne  7407  prarloclemarch2  7567  ltexprlemrl  7758  cauappcvgprlemladdrl  7805  caucvgprlemladdrl  7826  caucvgprlem1  7827  axpre-suploclemres  8049  uzind  9519  supinfneg  9751  infsupneg  9752  ixxssxr  10057  elfz0add  10277  fzoss1  10330  elfzoextl  10357  frecuzrdgrclt  10597  ccatval2  11092  swrdswrd  11196  pfxccatin12lem2a  11218  swrdccatin2  11220  pfxccatpfx2  11228  fsum3cvg  11804  isumrpcl  11920  fproddccvg  11998  reumodprminv  12691  issubmnd  13389  issubg2m  13640  eqgid  13677  issubrng2  14087  subrgdvds  14112  issubrg2  14118  lssats2  14291  rnglidlmmgm  14373  rnglidlmsgrp  14374  rnglidlrng  14375  mplbasss  14573  lmtopcnp  14837  txuni2  14843  tx1cn  14856  tx2cn  14857  txlm  14866  imasnopn  14886  xmetunirn  14945  mopnval  15029  metrest  15093  dedekindicc  15220  ivthdec  15231  limcimolemlt  15251  plyssc  15326  edgupgren  15845  bj-charfundc  15943  bj-nnord  16093