riotarab

Description: Restricted iota of a restricted abstraction. (Contributed by Scott Fenton, 8-Aug-2024)

		Ref	Expression
	Hypothesis	riotarab.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
	Assertion	riotarab	$⊢ (ι x \in \{y \in A \| ψ\} \| χ) = (ι x \in A \| (φ \land χ))$

Step	Hyp	Ref	Expression
1		riotarab.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
2	1	bicomd	$⊢ x = y \to (ψ \leftrightarrow φ)$
3	2	equcoms	$⊢ y = x \to (ψ \leftrightarrow φ)$
4	3	elrab	$⊢ x \in \{y \in A \| ψ\} \leftrightarrow (x \in A \land φ)$
5	4	anbi1i	$⊢ (x \in \{y \in A \| ψ\} \land χ) \leftrightarrow ((x \in A \land φ) \land χ)$
6		anass	$⊢ ((x \in A \land φ) \land χ) \leftrightarrow (x \in A \land (φ \land χ))$
7	5 6	bitri	$⊢ (x \in \{y \in A \| ψ\} \land χ) \leftrightarrow (x \in A \land (φ \land χ))$
8	7	iotabii	$⊢ (ι x \| (x \in \{y \in A \| ψ\} \land χ)) = (ι x \| (x \in A \land (φ \land χ)))$
9		df-riota	$⊢ (ι x \in \{y \in A \| ψ\} \| χ) = (ι x \| (x \in \{y \in A \| ψ\} \land χ))$
10		df-riota	$⊢ (ι x \in A \| (φ \land χ)) = (ι x \| (x \in A \land (φ \land χ)))$
11	8 9 10	3eqtr4i	$⊢ (ι x \in \{y \in A \| ψ\} \| χ) = (ι x \in A \| (φ \land χ))$

Metamath Proof Explorer