This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ \{x \in A \| x \in B\} = \{x \in B \| x \in A\}$
2		dfin5	$⊢ A \cap B = \{x \in A \| x \in B\}$
3		dfin5	$⊢ B \cap A = \{x \in B \| x \in A\}$
4	1 2 3	3eqtr4i	$⊢ A \cap B = B \cap A$