Theorem ssel 3147

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 3142	. . . . . 6 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
2	1	biimpi 120	. . . . 5 |- ( A C_ B -> A. x ( x e. A -> x e. B ) )
3	2	19.21bi 1556	. . . 4 |- ( A C_ B -> ( x e. A -> x e. B ) )
4	3	anim2d 337	. . 3 |- ( A C_ B -> ( ( x = C /\ x e. A ) -> ( x = C /\ x e. B ) ) )
5	4	eximdv 1878	. 2 |- ( A C_ B -> ( E. x ( x = C /\ x e. A ) -> E. x ( x = C /\ x e. B ) ) )
6		df-clel 2171	. 2 |- ( C e. A <-> E. x ( x = C /\ x e. A ) )
7		df-clel 2171	. 2 |- ( C e. B <-> E. x ( x = C /\ x e. B ) )
8	5, 6, 7	3imtr4g 205	1 |- ( A C_ B -> ( C e. A -> C e. B ) )

Syntax hints:   -> wi 4   /\ wa 104   A.wal 1351   = wceq 1353   E.wex 1490   e. wcel 2146   C_ wss 3127

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 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-11 1504  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-in 3133  df-ss 3140

This theorem is referenced by:  ssel2  3148  sseli  3149  sseld  3152  sstr2  3160  nelss  3214  ssrexf  3215  ssralv  3217  ssrexv  3218  ralss  3219  rexss  3220  ssconb  3266  sscon  3267  ssdif  3268  unss1  3302  ssrin  3358  difin2  3395  reuss2  3413  reupick  3417  sssnm  3750  uniss  3826  ss2iun  3897  ssiun  3924  iinss  3933  disjss2  3978  disjss1  3981  pwnss  4154  sspwb  4210  ssopab2b  4270  soss  4308  sucssel  4418  ssorduni  4480  onintonm  4510  onnmin  4561  ssnel  4562  wessep  4571  ssrel  4708  ssrel2  4710  ssrelrel  4720  xpss12  4727  cnvss  4793  dmss  4819  elreldm  4846  dmcosseq  4891  relssres  4938  iss  4946  resopab2  4947  issref  5003  ssrnres  5063  dfco2a  5121  cores  5124  funssres  5250  fununi  5276  funimaexglem  5291  dfimafn  5556  funimass4  5558  funimass3  5624  dff4im  5654  funfvima2  5740  funfvima3  5741  f1elima  5764  riotass2  5847  ssoprab2b  5922  resoprab2  5962  releldm2  6176  reldmtpos  6244  dmtpos  6247  rdgss  6374  ss2ixp  6701  fiintim  6918  negf1o  8313  lbreu  8873  lbinf  8876  eqreznegel  9585  negm  9586  iccsupr  9935  negfi  11202  sumrbdclem  11351  prodrbdclem  11545  fprodmodd  11615  mulgpropdg  12883  metrest  13575  bdop  14185  bj-nnen2lp  14264  exmidsbthrlem  14329