inrab2

Description: Intersection with a restricted class abstraction. (Contributed by NM, 19-Nov-2007)

		Ref	Expression
	Assertion	inrab2	$⊢ \{x \in A \| φ\} \cap B = \{x \in (A \cap B) \| φ\}$

Step	Hyp	Ref	Expression
1		df-rab	$⊢ \{x \in A \| φ\} = \{x \| (x \in A \land φ)\}$
2		abid1	$⊢ B = \{x \| x \in B\}$
3	1 2	ineq12i	$⊢ \{x \in A \| φ\} \cap B = \{x \| (x \in A \land φ)\} \cap \{x \| x \in B\}$
4		df-rab	$⊢ \{x \in (A \cap B) \| φ\} = \{x \| (x \in (A \cap B) \land φ)\}$
5		inab	$⊢ \{x \| (x \in A \land φ)\} \cap \{x \| x \in B\} = \{x \| ((x \in A \land φ) \land x \in B)\}$
6		elin	$⊢ x \in (A \cap B) \leftrightarrow (x \in A \land x \in B)$
7	6	anbi1i	$⊢ (x \in (A \cap B) \land φ) \leftrightarrow ((x \in A \land x \in B) \land φ)$
8		an32	$⊢ ((x \in A \land x \in B) \land φ) \leftrightarrow ((x \in A \land φ) \land x \in B)$
9	7 8	bitri	$⊢ (x \in (A \cap B) \land φ) \leftrightarrow ((x \in A \land φ) \land x \in B)$
10	9	abbii	$⊢ \{x \| (x \in (A \cap B) \land φ)\} = \{x \| ((x \in A \land φ) \land x \in B)\}$
11	5 10	eqtr4i	$⊢ \{x \| (x \in A \land φ)\} \cap \{x \| x \in B\} = \{x \| (x \in (A \cap B) \land φ)\}$
12	4 11	eqtr4i	$⊢ \{x \in (A \cap B) \| φ\} = \{x \| (x \in A \land φ)\} \cap \{x \| x \in B\}$
13	3 12	eqtr4i	$⊢ \{x \in A \| φ\} \cap B = \{x \in (A \cap B) \| φ\}$

Metamath Proof Explorer