Metamath Proof Explorer


Theorem eqabcb

Description: Equality of a class variable and a class abstraction. Commuted form of eqabb . (Contributed by NM, 20-Aug-1993)

Ref Expression
Assertion eqabcb x | φ = A x φ x A

Proof

Step Hyp Ref Expression
1 eqabb A = x | φ x x A φ
2 eqcom x | φ = A A = x | φ
3 bicom φ x A x A φ
4 3 albii x φ x A x x A φ
5 1 2 4 3bitr4i x | φ = A x φ x A