Theorem sseld 3192

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 3187	. 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 2176   C_ wss 3166

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179

This theorem is referenced by:  sselda  3193  sseldd  3194  ssneld  3195  elelpwi  3628  ssbrd  4088  uniopel  4302  onintonm  4566  sucprcreg  4598  ordsuc  4612  0elnn  4668  dmrnssfld  4942  nfunv  5305  opelf  5449  fvimacnv  5697  ffvelcdm  5715  resflem  5746  f1imass  5845  dftpos3  6350  nnmordi  6604  mapsn  6779  ixpf  6809  pw2f1odclem  6933  diffifi  6993  ordiso2  7139  difinfinf  7205  exmidapne  7374  prarloclemarch2  7534  ltexprlemrl  7725  cauappcvgprlemladdrl  7772  caucvgprlemladdrl  7793  caucvgprlem1  7794  axpre-suploclemres  8016  uzind  9486  supinfneg  9718  infsupneg  9719  ixxssxr  10024  elfz0add  10244  fzoss1  10297  elfzoextl  10322  frecuzrdgrclt  10562  ccatval2  11057  fsum3cvg  11722  isumrpcl  11838  fproddccvg  11916  reumodprminv  12609  issubmnd  13307  issubg2m  13558  eqgid  13595  issubrng2  14005  subrgdvds  14030  issubrg2  14036  lssats2  14209  rnglidlmmgm  14291  rnglidlmsgrp  14292  rnglidlrng  14293  mplbasss  14491  lmtopcnp  14755  txuni2  14761  tx1cn  14774  tx2cn  14775  txlm  14784  imasnopn  14804  xmetunirn  14863  mopnval  14947  metrest  15011  dedekindicc  15138  ivthdec  15149  limcimolemlt  15169  plyssc  15244  bj-charfundc  15781  bj-nnord  15931