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=B\leftrightarrow B=A$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢A=B\to A=B$$
2	1	eqcomd	$$⊢A=B\to B=A$$
3		id	$$⊢B=A\to B=A$$
4	3	eqcomd	$$⊢B=A\to A=B$$
5	2 4	impbii	$$⊢A=B\leftrightarrow B=A$$