Theorem ssel2 3188

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 3187	. 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 2176   C_ wss 3166

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179

This theorem is referenced by:  elnn  4655  funimass4  5631  fvelimab  5637  ssimaex  5642  funconstss  5700  rexima  5825  ralima  5826  1st2nd  6269  f1o2ndf1  6316  tfri1dALT  6439  eldju1st  7175  axsuploc  8147  lbinf  9023  dfinfre  9031  lbzbi  9739  elfzom1elp1fzo  10333  ssfzo12  10355  seq3split  10635  seqsplitg  10636  shftlem  11160  uzwodc  12391  subgintm  13567  subrngintm  14007  subrgintm  14038  tgcl  14569  neipsm  14659  txbasval  14772  elmopn2  14954  metrest  15011  cncfmet  15097  negcncf  15110  ply1term  15248  plyconst  15250  reeff1olem  15276