Metamath Proof Explorer

Theorem eqab

Description: One direction of eqabb is provable from fewer axioms. (Contributed by Wolf Lammen, 13-Feb-2025)

Ref Expression
Assertion eqab 
|- ( A. x ( x e. A <-> ph ) -> A = { x | ph } )

Proof

Step Hyp Ref Expression
1 abid1 
 |-  A = { x | x e. A }
2 abbi 
 |-  ( A. x ( x e. A <-> ph ) -> { x | x e. A } = { x | ph } )
3 1 2 eqtrid 
 |-  ( A. x ( x e. A <-> ph ) -> A = { x | ph } )