Metamath Proof Explorer


Theorem eqcom

Description: Commutative law for class equality. Theorem 6.5 of Quine p. 41. (Contributed by NM, 26-May-1993) (Proof shortened by Wolf Lammen, 19-Nov-2019)

Ref Expression
Assertion eqcom A=BB=A

Proof

Step Hyp Ref Expression
1 id A=BA=B
2 1 eqcomd A=BB=A
3 id B=AB=A
4 3 eqcomd B=AA=B
5 2 4 impbii A=BB=A