Metamath Proof Explorer


Theorem abeq1i

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 abeq1i.1 x | φ = A
Assertion abeq1i φ x A

Proof

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