Theorem ssel 3017

Description: Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
ssel	|- ( A C_ B -> ( C e. A -> C e. B ) )

Proof of Theorem ssel

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfss2 3012	. . . . . 6 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
2	1	biimpi 118	. . . . 5 |- ( A C_ B -> A. x ( x e. A -> x e. B ) )
3	2	19.21bi 1495	. . . 4 |- ( A C_ B -> ( x e. A -> x e. B ) )
4	3	anim2d 330	. . 3 |- ( A C_ B -> ( ( x = C /\ x e. A ) -> ( x = C /\ x e. B ) ) )
5	4	eximdv 1808	. 2 |- ( A C_ B -> ( E. x ( x = C /\ x e. A ) -> E. x ( x = C /\ x e. B ) ) )
6		df-clel 2084	. 2 |- ( C e. A <-> E. x ( x = C /\ x e. A ) )
7		df-clel 2084	. 2 |- ( C e. B <-> E. x ( x = C /\ x e. B ) )
8	5, 6, 7	3imtr4g 203	1 |- ( A C_ B -> ( C e. A -> C e. B ) )

Syntax hints:   -> wi 4   /\ wa 102   A.wal 1287   = wceq 1289   E.wex 1426   e. wcel 1438   C_ wss 2997

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 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-11 1442  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-in 3003  df-ss 3010

This theorem is referenced by:  ssel2  3018  sseli  3019  sseld  3022  sstr2  3030  ssralv  3083  ssrexv  3084  ralss  3085  rexss  3086  ssconb  3131  sscon  3132  ssdif  3133  unss1  3167  ssrin  3223  difin2  3259  reuss2  3277  reupick  3281  sssnm  3593  uniss  3669  ss2iun  3740  ssiun  3767  iinss  3776  disjss2  3817  disjss1  3820  pwnss  3986  sspwb  4034  ssopab2b  4094  soss  4132  sucssel  4242  ssorduni  4294  onintonm  4324  onnmin  4374  ssnel  4375  wessep  4383  ssrel  4514  ssrel2  4516  ssrelrel  4526  xpss12  4533  cnvss  4597  dmss  4623  elreldm  4649  dmcosseq  4692  relssres  4737  iss  4745  resopab2  4746  issref  4801  ssrnres  4860  dfco2a  4918  cores  4921  funssres  5042  fununi  5068  funimaexglem  5083  dfimafn  5337  funimass4  5339  funimass3  5399  dff4im  5429  funfvima2  5509  funfvima3  5510  f1elima  5534  riotass2  5616  ssoprab2b  5688  resoprab2  5724  releldm2  5937  reldmtpos  6000  dmtpos  6003  rdgss  6130  negf1o  7839  lbreu  8378  lbinf  8381  eqreznegel  9068  negm  9069  iccsupr  9353  negfi  10623  isumrblem  10729  bdop  11423  bj-nnen2lp  11506  exmidsbthrlem  11569