Theorem sseld 3241

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 3236	. 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 2205   C_ wss 3214

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227

This theorem is referenced by:  sselda  3242  sseldd  3243  ssneld  3244  elelpwi  3686  ssbrd  4157  uniopel  4378  onintonm  4644  sucprcreg  4676  ordsuc  4690  0elnn  4746  dmrnssfld  5025  nfunv  5390  opelf  5540  fvimacnv  5798  ffvelcdm  5815  resflem  5846  f1imass  5953  suppssrst  6474  suppssrgst  6475  dftpos3  6506  nnmordi  6762  mapsnd  6936  mapsn  6938  ixpf  6968  pw2f1odclem  7100  diffifi  7164  ordiso2  7339  difinfinf  7405  exmidapne  7590  prarloclemarch2  7750  ltexprlemrl  7941  cauappcvgprlemladdrl  7988  caucvgprlemladdrl  8009  caucvgprlem1  8010  axpre-suploclemres  8232  uzind  9707  supinfneg  9945  infsupneg  9946  ixxssxr  10252  elfz0add  10476  fzoss1  10529  elfzoextl  10558  frecuzrdgrclt  10801  ccatval2  11311  swrdswrd  11422  pfxccatin12lem2a  11444  swrdccatin2  11446  pfxccatpfx2  11454  fsum3cvg  12089  isumrpcl  12205  fproddccvg  12283  reumodprminv  12976  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemimin  13193  issubmnd  13703  issubg2m  13942  eqgid  13979  issubrng2  14456  subrgdvds  14481  issubrg2  14487  lssats2  14688  rnglidlmmgm  14770  rnglidlmsgrp  14771  rnglidlrng  14772  mplbasss  14977  lmtopcnp  15241  txuni2  15247  tx1cn  15260  tx2cn  15261  txlm  15270  imasnopn  15290  xmetunirn  15349  mopnval  15433  metrest  15497  dedekindicc  15624  ivthdec  15635  limcimolemlt  15655  plyssc  15730  edgupgren  16262  subgreldmiedg  16390  clwwlkccatlem  16521  eupth2lemsfi  16599  bj-charfundc  16704  bj-nnord  16854