Metamath Proof Explorer


Theorem eqabcri

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

Ref Expression
Hypothesis eqabcri.1 x | φ = A
Assertion eqabcri φ x A

Proof

Step Hyp Ref Expression
1 eqabcri.1 x | φ = A
2 1 eqcomi A = x | φ
3 2 eqabri x A φ
4 3 bicomi φ x A