Theorem abid2 2308

Description: A simplification of class abstraction. Theorem 5.2 of [Quine] p. 35. (Contributed by NM, 26-Dec-1993.)

Assertion

Ref	Expression
abid2	|- { x | x e. A } = A

Distinct variable group:   x, A

Proof of Theorem abid2

Step	Hyp	Ref	Expression
1		biid 171	. . 3 |- ( x e. A <-> x e. A )
2	1	abbi2i 2302	. 2 |- A = { x | x e. A }
3	2	eqcomi 2191	1 |- { x | x e. A } = A

Syntax hints:   = wceq 1363   e. wcel 2158   {cab 2173

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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-11 1516  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183

This theorem is referenced by:  csbid  3077  abss  3236  ssab  3237  abssi  3242  notab  3417  inrab2  3420  dfrab2  3422  dfrab3  3423  notrab  3424  eusn  3678  dfopg  3788  iunid  3954  csbexga  4143  imai  4996  dffv4g  5524  frec0g  6411  dfixp  6713  euen1b  6816  acfun  7219  ccfunen  7276