Theorem uncom

Description: Commutative law for union of classes. Exercise 6 of TakeutiZaring p. 17. (Contributed by NM, 25-Jun-1998) (Proof shortened by Andrew Salmon, 26-Jun-2011)

	Ref	Expression
Assertion	uncom	$$⊢A\cup B=B\cup A$$

Proof

Step	Hyp	Ref	Expression
1		orcom	$$⊢\left(x\in A\vee x\in B\right)\leftrightarrow \left(x\in B\vee x\in A\right)$$
2		elun	$$⊢x\in \left(B\cup A\right)\leftrightarrow \left(x\in B\vee x\in A\right)$$
3	1 2	bitr4i	$$⊢\left(x\in A\vee x\in B\right)\leftrightarrow x\in \left(B\cup A\right)$$
4	3	uneqri	$$⊢A\cup B=B\cup A$$