Theorem ssel 3096

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 3091	. . . . . 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 1538	. . . 4 |- ( A C_ B -> ( x e. A -> x e. B ) )
4	3	anim2d 335	. . 3 |- ( A C_ B -> ( ( x = C /\ x e. A ) -> ( x = C /\ x e. B ) ) )
5	4	eximdv 1853	. 2 |- ( A C_ B -> ( E. x ( x = C /\ x e. A ) -> E. x ( x = C /\ x e. B ) ) )
6		df-clel 2136	. 2 |- ( C e. A <-> E. x ( x = C /\ x e. A ) )
7		df-clel 2136	. 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 1330   = wceq 1332   E.wex 1469   e. wcel 1481   C_ wss 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-in 3082  df-ss 3089

This theorem is referenced by:  ssel2  3097  sseli  3098  sseld  3101  sstr2  3109  nelss  3163  ssrexf  3164  ssralv  3166  ssrexv  3167  ralss  3168  rexss  3169  ssconb  3214  sscon  3215  ssdif  3216  unss1  3250  ssrin  3306  difin2  3343  reuss2  3361  reupick  3365  sssnm  3689  uniss  3765  ss2iun  3836  ssiun  3863  iinss  3872  disjss2  3917  disjss1  3920  pwnss  4091  sspwb  4146  ssopab2b  4206  soss  4244  sucssel  4354  ssorduni  4411  onintonm  4441  onnmin  4491  ssnel  4492  wessep  4500  ssrel  4635  ssrel2  4637  ssrelrel  4647  xpss12  4654  cnvss  4720  dmss  4746  elreldm  4773  dmcosseq  4818  relssres  4865  iss  4873  resopab2  4874  issref  4929  ssrnres  4989  dfco2a  5047  cores  5050  funssres  5173  fununi  5199  funimaexglem  5214  dfimafn  5478  funimass4  5480  funimass3  5544  dff4im  5574  funfvima2  5658  funfvima3  5659  f1elima  5682  riotass2  5764  ssoprab2b  5836  resoprab2  5876  releldm2  6091  reldmtpos  6158  dmtpos  6161  rdgss  6288  ss2ixp  6613  fiintim  6825  negf1o  8168  lbreu  8727  lbinf  8730  eqreznegel  9433  negm  9434  iccsupr  9779  negfi  11031  sumrbdclem  11178  prodrbdclem  11372  metrest  12714  bdop  13244  bj-nnen2lp  13323  exmidsbthrlem  13392