Theorem abid2 2200

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 169	. . 3 |- ( x e. A <-> x e. A )
2	1	abbi2i 2194	. 2 |- A = { x | x e. A }
3	2	eqcomi 2086	1 |- { x | x e. A } = A

Syntax hints:   = wceq 1285   e. wcel 1434   {cab 2068

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-11 1438  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064

This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078

This theorem is referenced by:  csbid  2916  abss  3064  ssab  3065  abssi  3070  notab  3241  inrab2  3244  dfrab2  3246  dfrab3  3247  notrab  3248  eusn  3474  dfopg  3576  iunid  3741  csbexga  3914  imai  4711  dffv4g  5206  frec0g  6046  euen1b  6350