Theorem abid2 2261

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 2255	. 2 |- A = { x | x e. A }
3	2	eqcomi 2144	1 |- { x | x e. A } = A

Syntax hints:   = wceq 1332   e. wcel 1481   {cab 2126

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

This theorem is referenced by:  csbid  3015  abss  3171  ssab  3172  abssi  3177  notab  3351  inrab2  3354  dfrab2  3356  dfrab3  3357  notrab  3358  eusn  3605  dfopg  3711  iunid  3876  csbexga  4064  imai  4903  dffv4g  5426  frec0g  6302  dfixp  6602  euen1b  6705  acfun  7080  ccfunen  7096