Theorem incom

Description: Commutative law for intersection of classes. Exercise 7 of TakeutiZaring p. 17. (Contributed by NM, 21-Jun-1993) (Proof shortened by SN, 12-Dec-2023)

	Ref	Expression
Assertion	incom	$$⊢A\cap B=B\cap A$$

Proof

Step	Hyp	Ref	Expression
1		rabswap	$$⊢\left\{x\in A|x\in B\right\}=\left\{x\in B|x\in A\right\}$$
2		dfin5	$$⊢A\cap B=\left\{x\in A|x\in B\right\}$$
3		dfin5	$$⊢B\cap A=\left\{x\in B|x\in A\right\}$$
4	1 2 3	3eqtr4i	$$⊢A\cap B=B\cap A$$