Theorem sseld 3223

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 3218	. 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 2200   C_ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  sselda  3224  sseldd  3225  ssneld  3226  elelpwi  3661  ssbrd  4126  uniopel  4343  onintonm  4609  sucprcreg  4641  ordsuc  4655  0elnn  4711  dmrnssfld  4987  nfunv  5351  opelf  5496  fvimacnv  5750  ffvelcdm  5768  resflem  5799  f1imass  5898  dftpos3  6408  nnmordi  6662  mapsn  6837  ixpf  6867  pw2f1odclem  6995  diffifi  7056  ordiso2  7202  difinfinf  7268  exmidapne  7446  prarloclemarch2  7606  ltexprlemrl  7797  cauappcvgprlemladdrl  7844  caucvgprlemladdrl  7865  caucvgprlem1  7866  axpre-suploclemres  8088  uzind  9558  supinfneg  9790  infsupneg  9791  ixxssxr  10096  elfz0add  10316  fzoss1  10369  elfzoextl  10397  frecuzrdgrclt  10637  ccatval2  11133  swrdswrd  11237  pfxccatin12lem2a  11259  swrdccatin2  11261  pfxccatpfx2  11269  fsum3cvg  11889  isumrpcl  12005  fproddccvg  12083  reumodprminv  12776  issubmnd  13475  issubg2m  13726  eqgid  13763  issubrng2  14174  subrgdvds  14199  issubrg2  14205  lssats2  14378  rnglidlmmgm  14460  rnglidlmsgrp  14461  rnglidlrng  14462  mplbasss  14660  lmtopcnp  14924  txuni2  14930  tx1cn  14943  tx2cn  14944  txlm  14953  imasnopn  14973  xmetunirn  15032  mopnval  15116  metrest  15180  dedekindicc  15307  ivthdec  15318  limcimolemlt  15338  plyssc  15413  edgupgren  15939  bj-charfundc  16171  bj-nnord  16321