Theorem ssel2 3150

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 3149	. 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 2148   C_ wss 3129

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 3135  df-ss 3142

This theorem is referenced by:  elnn  4605  funimass4  5566  fvelimab  5572  ssimaex  5577  funconstss  5634  rexima  5755  ralima  5756  1st2nd  6181  f1o2ndf1  6228  tfri1dALT  6351  eldju1st  7069  axsuploc  8029  lbinf  8904  dfinfre  8912  lbzbi  9615  elfzom1elp1fzo  10201  ssfzo12  10223  seq3split  10478  shftlem  10824  uzwodc  12037  subgintm  13056  subrgintm  13362  tgcl  13534  neipsm  13624  txbasval  13737  elmopn2  13919  metrest  13976  cncfmet  14049  negcncf  14058  reeff1olem  14162