bj-inrab

		Ref	Expression
	Assertion	bj-inrab	$⊢ \{x \in A \| φ\} \cap \{x \in B \| ψ\} = \{x \in (A \cap B) \| (φ \land ψ)\}$

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

Metamath Proof Explorer