Metamath Proof Explorer

Theorem abid2

Description: A simplification of class abstraction. Commuted form of abid1 . See comments there. (Contributed by NM, 26-Dec-1993)

Ref Expression
Assertion abid2 
|- { x | x e. A } = A

Proof

Step Hyp Ref Expression
1 abid1 
 |-  A = { x | x e. A }
2 1 eqcomi 
 |-  { x | x e. A } = A