Metamath Proof Explorer

Theorem riotabidv

Description: Formula-building deduction for restricted iota. (Contributed by NM, 15-Sep-2011)

		Ref	Expression
	Hypothesis	riotabidv.1	$⊢ φ \to (ψ \leftrightarrow χ)$
	Assertion	riotabidv	$⊢ φ \to (ι x \in A \| ψ) = (ι x \in A \| χ)$

Step	Hyp	Ref	Expression
1		riotabidv.1	$⊢ φ \to (ψ \leftrightarrow χ)$
2	1	anbi2d	$⊢ φ \to ((x \in A \land ψ) \leftrightarrow (x \in A \land χ))$
3	2	iotabidv	$⊢ φ \to (ι x \| (x \in A \land ψ)) = (ι x \| (x \in A \land χ))$
4		df-riota	$⊢ (ι x \in A \| ψ) = (ι x \| (x \in A \land ψ))$
5		df-riota	$⊢ (ι x \in A \| χ) = (ι x \| (x \in A \land χ))$
6	3 4 5	3eqtr4g	$⊢ φ \to (ι x \in A \| ψ) = (ι x \in A \| χ)$