Metamath Proof Explorer


Theorem eqabri

Description: Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 3-Apr-1996) (Proof shortened by Wolf Lammen, 15-Nov-2019)

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

Proof

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