inass

Description: Associative law for intersection of classes. Exercise 9 of TakeutiZaring p. 17. (Contributed by NM, 3-May-1994)

		Ref	Expression
	Assertion	inass	$⊢ (A \cap B) \cap C = A \cap (B \cap C)$

Step	Hyp	Ref	Expression
1		anass	$⊢ ((x \in A \land x \in B) \land x \in C) \leftrightarrow (x \in A \land (x \in B \land x \in C))$
2		elin	$⊢ x \in (B \cap C) \leftrightarrow (x \in B \land x \in C)$
3	2	anbi2i	$⊢ (x \in A \land x \in (B \cap C)) \leftrightarrow (x \in A \land (x \in B \land x \in C))$
4	1 3	bitr4i	$⊢ ((x \in A \land x \in B) \land x \in C) \leftrightarrow (x \in A \land x \in (B \cap C))$
5		elin	$⊢ x \in (A \cap B) \leftrightarrow (x \in A \land x \in B)$
6	5	anbi1i	$⊢ (x \in (A \cap B) \land x \in C) \leftrightarrow ((x \in A \land x \in B) \land x \in C)$
7		elin	$⊢ x \in (A \cap (B \cap C)) \leftrightarrow (x \in A \land x \in (B \cap C))$
8	4 6 7	3bitr4i	$⊢ (x \in (A \cap B) \land x \in C) \leftrightarrow x \in (A \cap (B \cap C))$
9	8	ineqri	$⊢ (A \cap B) \cap C = A \cap (B \cap C)$

Metamath Proof Explorer