inrab

Description: Intersection of two restricted class abstractions. (Contributed by NM, 1-Sep-2006)

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

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

Metamath Proof Explorer