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  4087  uniopel  4301  onintonm  4565  sucprcreg  4597  ordsuc  4611  0elnn  4667  dmrnssfld  4941  nfunv  5304  opelf  5447  fvimacnv  5695  ffvelcdm  5713  resflem  5744  f1imass  5843  dftpos3  6348  nnmordi  6602  mapsn  6777  ixpf  6807  pw2f1odclem  6931  diffifi  6991  ordiso2  7137  difinfinf  7203  exmidapne  7372  prarloclemarch2  7532  ltexprlemrl  7723  cauappcvgprlemladdrl  7770  caucvgprlemladdrl  7791  caucvgprlem1  7792  axpre-suploclemres  8014  uzind  9484  supinfneg  9716  infsupneg  9717  ixxssxr  10022  elfz0add  10242  fzoss1  10295  elfzoextl  10320  frecuzrdgrclt  10560  ccatval2  11054  fsum3cvg  11689  isumrpcl  11805  fproddccvg  11883  reumodprminv  12576  issubmnd  13274  issubg2m  13525  eqgid  13562  issubrng2  13972  subrgdvds  13997  issubrg2  14003  lssats2  14176  rnglidlmmgm  14258  rnglidlmsgrp  14259  rnglidlrng  14260  mplbasss  14458  lmtopcnp  14722  txuni2  14728  tx1cn  14741  tx2cn  14742  txlm  14751  imasnopn  14771  xmetunirn  14830  mopnval  14914  metrest  14978  dedekindicc  15105  ivthdec  15116  limcimolemlt  15136  plyssc  15211  bj-charfundc  15744  bj-nnord  15894