Theorem sseld 3156

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 3151	. 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 2148   C_ wss 3131

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3137  df-ss 3144

This theorem is referenced by:  sselda  3157  sseldd  3158  ssneld  3159  elelpwi  3589  ssbrd  4048  uniopel  4258  onintonm  4518  sucprcreg  4550  ordsuc  4564  0elnn  4620  dmrnssfld  4892  nfunv  5251  opelf  5389  fvimacnv  5633  ffvelcdm  5651  resflem  5682  f1imass  5777  dftpos3  6265  nnmordi  6519  mapsn  6692  ixpf  6722  diffifi  6896  ordiso2  7036  difinfinf  7102  exmidapne  7261  prarloclemarch2  7420  ltexprlemrl  7611  cauappcvgprlemladdrl  7658  caucvgprlemladdrl  7679  caucvgprlem1  7680  axpre-suploclemres  7902  uzind  9366  supinfneg  9597  infsupneg  9598  ixxssxr  9902  elfz0add  10122  fzoss1  10173  frecuzrdgrclt  10417  fsum3cvg  11388  isumrpcl  11504  fproddccvg  11582  reumodprminv  12255  issubmnd  12848  issubg2m  13054  eqgid  13090  subrgdvds  13361  issubrg2  13367  lssats2  13505  lmtopcnp  13835  txuni2  13841  tx1cn  13854  tx2cn  13855  txlm  13864  imasnopn  13884  xmetunirn  13943  mopnval  14027  metrest  14091  dedekindicc  14196  ivthdec  14207  limcimolemlt  14218  bj-charfundc  14645  bj-nnord  14795