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 <-> B = A )

Proof

Step	Hyp	Ref	Expression
1		id	|- ( A = B -> A = B )
2	1	eqcomd	|- ( A = B -> B = A )
3		id	|- ( B = A -> B = A )
4	3	eqcomd	|- ( B = A -> A = B )
5	2 4	impbii	|- ( A = B <-> B = A )