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 φ A = x | ψ
Assertion eqabrd φ x A ψ

Proof

Step Hyp Ref Expression
1 eqabrd.1 φ A = x | ψ
2 1 eleq2d φ x A x x | ψ
3 abid x x | ψ ψ
4 2 3 bitrdi φ x A ψ