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	⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		rabswap	⊢ { 𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵 } = { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝐴 }
2		dfin5	⊢ ( 𝐴 ∩ 𝐵 ) = { 𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵 }
3		dfin5	⊢ ( 𝐵 ∩ 𝐴 ) = { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝐴 }
4	1 2 3	3eqtr4i	⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐴 )