Theorem ssel2 3175

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 3174	. 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 2164   C_ wss 3154

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 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3160  df-ss 3167

This theorem is referenced by:  elnn  4639  funimass4  5608  fvelimab  5614  ssimaex  5619  funconstss  5677  rexima  5798  ralima  5799  1st2nd  6236  f1o2ndf1  6283  tfri1dALT  6406  eldju1st  7132  axsuploc  8094  lbinf  8969  dfinfre  8977  lbzbi  9684  elfzom1elp1fzo  10272  ssfzo12  10294  seq3split  10562  seqsplitg  10563  shftlem  10963  uzwodc  12177  subgintm  13271  subrngintm  13711  subrgintm  13742  tgcl  14243  neipsm  14333  txbasval  14446  elmopn2  14628  metrest  14685  cncfmet  14771  negcncf  14784  ply1term  14922  plyconst  14924  reeff1olem  14947