Theorem sseld 3178

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 3173	. 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 2164   C_ wss 3153

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3159  df-ss 3166

This theorem is referenced by:  sselda  3179  sseldd  3180  ssneld  3181  elelpwi  3613  ssbrd  4072  uniopel  4285  onintonm  4549  sucprcreg  4581  ordsuc  4595  0elnn  4651  dmrnssfld  4925  nfunv  5287  opelf  5425  fvimacnv  5673  ffvelcdm  5691  resflem  5722  f1imass  5817  dftpos3  6315  nnmordi  6569  mapsn  6744  ixpf  6774  pw2f1odclem  6890  diffifi  6950  ordiso2  7094  difinfinf  7160  exmidapne  7320  prarloclemarch2  7479  ltexprlemrl  7670  cauappcvgprlemladdrl  7717  caucvgprlemladdrl  7738  caucvgprlem1  7739  axpre-suploclemres  7961  uzind  9428  supinfneg  9660  infsupneg  9661  ixxssxr  9966  elfz0add  10186  fzoss1  10238  frecuzrdgrclt  10486  fsum3cvg  11521  isumrpcl  11637  fproddccvg  11715  reumodprminv  12391  issubmnd  13023  issubg2m  13259  eqgid  13296  issubrng2  13706  subrgdvds  13731  issubrg2  13737  lssats2  13910  rnglidlmmgm  13992  rnglidlmsgrp  13993  rnglidlrng  13994  lmtopcnp  14418  txuni2  14424  tx1cn  14437  tx2cn  14438  txlm  14447  imasnopn  14467  xmetunirn  14526  mopnval  14610  metrest  14674  dedekindicc  14787  ivthdec  14798  limcimolemlt  14818  plyssc  14885  bj-charfundc  15300  bj-nnord  15450