Theorem ssel 3041

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 3036	. . . . . 6 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
2	1	biimpi 119	. . . . 5 |- ( A C_ B -> A. x ( x e. A -> x e. B ) )
3	2	19.21bi 1505	. . . 4 |- ( A C_ B -> ( x e. A -> x e. B ) )
4	3	anim2d 333	. . 3 |- ( A C_ B -> ( ( x = C /\ x e. A ) -> ( x = C /\ x e. B ) ) )
5	4	eximdv 1819	. 2 |- ( A C_ B -> ( E. x ( x = C /\ x e. A ) -> E. x ( x = C /\ x e. B ) ) )
6		df-clel 2096	. 2 |- ( C e. A <-> E. x ( x = C /\ x e. A ) )
7		df-clel 2096	. 2 |- ( C e. B <-> E. x ( x = C /\ x e. B ) )
8	5, 6, 7	3imtr4g 204	1 |- ( A C_ B -> ( C e. A -> C e. B ) )

Syntax hints:   -> wi 4   /\ wa 103   A.wal 1297   = wceq 1299   E.wex 1436   e. wcel 1448   C_ wss 3021

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-11 1452  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-in 3027  df-ss 3034

This theorem is referenced by:  ssel2  3042  sseli  3043  sseld  3046  sstr2  3054  ssralv  3108  ssrexv  3109  ralss  3110  rexss  3111  ssconb  3156  sscon  3157  ssdif  3158  unss1  3192  ssrin  3248  difin2  3285  reuss2  3303  reupick  3307  sssnm  3628  uniss  3704  ss2iun  3775  ssiun  3802  iinss  3811  disjss2  3855  disjss1  3858  pwnss  4023  sspwb  4076  ssopab2b  4136  soss  4174  sucssel  4284  ssorduni  4341  onintonm  4371  onnmin  4421  ssnel  4422  wessep  4430  ssrel  4565  ssrel2  4567  ssrelrel  4577  xpss12  4584  cnvss  4650  dmss  4676  elreldm  4703  dmcosseq  4746  relssres  4793  iss  4801  resopab2  4802  issref  4857  ssrnres  4917  dfco2a  4975  cores  4978  funssres  5101  fununi  5127  funimaexglem  5142  dfimafn  5402  funimass4  5404  funimass3  5468  dff4im  5498  funfvima2  5582  funfvima3  5583  f1elima  5606  riotass2  5688  ssoprab2b  5760  resoprab2  5800  releldm2  6013  reldmtpos  6080  dmtpos  6083  rdgss  6210  ss2ixp  6535  fiintim  6746  negf1o  8011  lbreu  8561  lbinf  8564  eqreznegel  9256  negm  9257  iccsupr  9590  negfi  10838  sumrbdclem  10984  metrest  12434  bdop  12654  bj-nnen2lp  12737  exmidsbthrlem  12801