rabrab

Description: Abstract builder restricted to another restricted abstract builder. (Contributed by Thierry Arnoux, 30-Aug-2017)

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

Step	Hyp	Ref	Expression
1		rabid	$⊢ x \in \{x \in A \| φ\} \leftrightarrow (x \in A \land φ)$
2	1	anbi1i	$⊢ (x \in \{x \in A \| φ\} \land ψ) \leftrightarrow ((x \in A \land φ) \land ψ)$
3		anass	$⊢ ((x \in A \land φ) \land ψ) \leftrightarrow (x \in A \land (φ \land ψ))$
4	2 3	bitri	$⊢ (x \in \{x \in A \| φ\} \land ψ) \leftrightarrow (x \in A \land (φ \land ψ))$
5	4	abbii	$⊢ \{x \| (x \in \{x \in A \| φ\} \land ψ)\} = \{x \| (x \in A \land (φ \land ψ))\}$
6		df-rab	$⊢ \{x \in \{x \in A \| φ\} \| ψ\} = \{x \| (x \in \{x \in A \| φ\} \land ψ)\}$
7		df-rab	$⊢ \{x \in A \| (φ \land ψ)\} = \{x \| (x \in A \land (φ \land ψ))\}$
8	5 6 7	3eqtr4i	$⊢ \{x \in \{x \in A \| φ\} \| ψ\} = \{x \in A \| (φ \land ψ)\}$

Metamath Proof Explorer