Metamath Proof Explorer


Theorem eqabrd

Description: Equality of a class variable and a class abstraction (deduction form of eqabb ). (Contributed by NM, 16-Nov-1995)

Ref Expression
Hypothesis eqabrd.1 ( 𝜑𝐴 = { 𝑥𝜓 } )
Assertion eqabrd ( 𝜑 → ( 𝑥𝐴𝜓 ) )

Proof

Step Hyp Ref Expression
1 eqabrd.1 ( 𝜑𝐴 = { 𝑥𝜓 } )
2 1 eleq2d ( 𝜑 → ( 𝑥𝐴𝑥 ∈ { 𝑥𝜓 } ) )
3 abid ( 𝑥 ∈ { 𝑥𝜓 } ↔ 𝜓 )
4 2 3 bitrdi ( 𝜑 → ( 𝑥𝐴𝜓 ) )