Metamath Proof Explorer


Theorem eqabi

Description: Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 26-May-1993) Avoid ax-11 . (Revised by Wolf Lammen, 6-May-2023)

Ref Expression
Hypothesis eqabi.1 ( 𝑥𝐴𝜑 )
Assertion eqabi 𝐴 = { 𝑥𝜑 }

Proof

Step Hyp Ref Expression
1 eqabi.1 ( 𝑥𝐴𝜑 )
2 1 a1i ( ⊤ → ( 𝑥𝐴𝜑 ) )
3 2 eqabdv ( ⊤ → 𝐴 = { 𝑥𝜑 } )
4 3 mptru 𝐴 = { 𝑥𝜑 }