Theorem abid2 2296

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

Syntax hints:   = wceq 1353   e. wcel 2146   {cab 2161

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 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-11 1504  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171

This theorem is referenced by:  csbid  3063  abss  3222  ssab  3223  abssi  3228  notab  3403  inrab2  3406  dfrab2  3408  dfrab3  3409  notrab  3410  eusn  3663  dfopg  3772  iunid  3937  csbexga  4126  imai  4977  dffv4g  5504  frec0g  6388  dfixp  6690  euen1b  6793  acfun  7196  ccfunen  7238