Metamath Proof Explorer


Theorem abid2f

Description: A simplification of class abstraction. Theorem 5.2 of Quine p. 35. (Contributed by NM, 5-Sep-2011) (Revised by Mario Carneiro, 7-Oct-2016) (Proof shortened by Wolf Lammen, 26-Feb-2025)

Ref Expression
Hypothesis abid2f.1
|- F/_ x A
Assertion abid2f
|- { x | x e. A } = A

Proof

Step Hyp Ref Expression
1 abid2f.1
 |-  F/_ x A
2 1 eqabf
 |-  ( A = { x | x e. A } <-> A. x ( x e. A <-> x e. A ) )
3 biid
 |-  ( x e. A <-> x e. A )
4 2 3 mpgbir
 |-  A = { x | x e. A }
5 4 eqcomi
 |-  { x | x e. A } = A