Theorem ssel2 2995

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 2994	. 2 |- ( A C_ B -> ( C e. A -> C e. B ) )
2	1	imp 122	1 |- ( ( A C_ B /\ C e. A ) -> C e. B )

Syntax hints:   -> wi 4   /\ wa 102   e. wcel 1434   C_ wss 2974

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-11 1438  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064

This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-in 2980  df-ss 2987

This theorem is referenced by:  elnn  4354  funimass4  5256  fvelimab  5261  ssimaex  5266  funconstss  5317  rexima  5426  ralima  5427  1st2nd  5838  f1o2ndf1  5880  tfri1dALT  6000  lbinf  8093  dfinfre  8101  lbzbi  8782  elfzom1elp1fzo  9288  ssfzo12  9310  iseqsplit  9554  shftlem  9842