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 ( ∀ 𝑥 ( 𝑥𝐴𝜑 ) → 𝐴 = { 𝑥𝜑 } )

Proof

Step Hyp Ref Expression
1 abid1 𝐴 = { 𝑥𝑥𝐴 }
2 abbi ( ∀ 𝑥 ( 𝑥𝐴𝜑 ) → { 𝑥𝑥𝐴 } = { 𝑥𝜑 } )
3 1 2 eqtrid ( ∀ 𝑥 ( 𝑥𝐴𝜑 ) → 𝐴 = { 𝑥𝜑 } )