Theorem abid2 2351

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

Syntax hints:   = wceq 1397   e. wcel 2201   {cab 2216

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226

This theorem is referenced by:  csbid  3134  abss  3295  ssab  3296  abssi  3301  notab  3476  inrab2  3479  dfrab2  3481  dfrab3  3482  notrab  3483  eusn  3746  dfopg  3861  iunid  4027  csbexga  4218  imai  5094  dffv4g  5639  frec0g  6568  dfixp  6874  euen1b  6982  modom2  7000  acfun  7427  ccfunen  7488