Theorem ssel2 3165

Description: Membership relationships follow from a subclass relationship. (Contributed by NM, 7-Jun-2004.)

Assertion

Ref	Expression
ssel2	|- ( ( A C_ B /\ C e. A ) -> C e. B )

Proof of Theorem ssel2

Step	Hyp	Ref	Expression
1		ssel 3164	. 2 |- ( A C_ B -> ( C e. A -> C e. B ) )
2	1	imp 124	1 |- ( ( A C_ B /\ C e. A ) -> C e. B )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2160   C_ wss 3144

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 2171

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-in 3150  df-ss 3157

This theorem is referenced by:  elnn  4623  funimass4  5587  fvelimab  5593  ssimaex  5598  funconstss  5655  rexima  5776  ralima  5777  1st2nd  6206  f1o2ndf1  6253  tfri1dALT  6376  eldju1st  7100  axsuploc  8060  lbinf  8935  dfinfre  8943  lbzbi  9646  elfzom1elp1fzo  10232  ssfzo12  10254  seq3split  10510  shftlem  10857  uzwodc  12070  subgintm  13137  subrngintm  13559  subrgintm  13590  tgcl  14021  neipsm  14111  txbasval  14224  elmopn2  14406  metrest  14463  cncfmet  14536  negcncf  14545  reeff1olem  14649