Theorem sseld 3166

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 3161	. 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 2158   C_ wss 3141

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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-11 1516  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-in 3147  df-ss 3154

This theorem is referenced by:  sselda  3167  sseldd  3168  ssneld  3169  elelpwi  3599  ssbrd  4058  uniopel  4268  onintonm  4528  sucprcreg  4560  ordsuc  4574  0elnn  4630  dmrnssfld  4902  nfunv  5261  opelf  5399  fvimacnv  5644  ffvelcdm  5662  resflem  5693  f1imass  5788  dftpos3  6277  nnmordi  6531  mapsn  6704  ixpf  6734  diffifi  6908  ordiso2  7048  difinfinf  7114  exmidapne  7273  prarloclemarch2  7432  ltexprlemrl  7623  cauappcvgprlemladdrl  7670  caucvgprlemladdrl  7691  caucvgprlem1  7692  axpre-suploclemres  7914  uzind  9378  supinfneg  9609  infsupneg  9610  ixxssxr  9914  elfz0add  10134  fzoss1  10185  frecuzrdgrclt  10429  fsum3cvg  11400  isumrpcl  11516  fproddccvg  11594  reumodprminv  12267  issubmnd  12865  issubg2m  13081  eqgid  13118  issubrng2  13430  subrgdvds  13455  issubrg2  13461  lssats2  13603  rnglidlmmgm  13685  rnglidlmsgrp  13686  rnglidlrng  13687  lmtopcnp  14046  txuni2  14052  tx1cn  14065  tx2cn  14066  txlm  14075  imasnopn  14095  xmetunirn  14154  mopnval  14238  metrest  14302  dedekindicc  14407  ivthdec  14418  limcimolemlt  14429  bj-charfundc  14856  bj-nnord  15006