Theorem abid2 2260

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 170	. . 3 |- ( x e. A <-> x e. A )
2	1	abbi2i 2254	. 2 |- A = { x | x e. A }
3	2	eqcomi 2143	1 |- { x | x e. A } = A

Syntax hints:   = wceq 1331   e. wcel 1480   {cab 2125

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 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135

This theorem is referenced by:  csbid  3011  abss  3166  ssab  3167  abssi  3172  notab  3346  inrab2  3349  dfrab2  3351  dfrab3  3352  notrab  3353  eusn  3597  dfopg  3703  iunid  3868  csbexga  4056  imai  4895  dffv4g  5418  frec0g  6294  dfixp  6594  euen1b  6697  acfun  7063  ccfunen  7079