cbvriotadavw

Description: Change bound variable in a restricted description binder. Deduction form. (Contributed by GG, 14-Aug-2025)

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

Step	Hyp	Ref	Expression
1		cbvriotadavw.1	$⊢ (φ \land x = y) \to (ψ \leftrightarrow χ)$
2		eleq1w	$⊢ x = y \to (x \in A \leftrightarrow y \in A)$
3	2	adantl	$⊢ (φ \land x = y) \to (x \in A \leftrightarrow y \in A)$
4	3 1	anbi12d	$⊢ (φ \land x = y) \to ((x \in A \land ψ) \leftrightarrow (y \in A \land χ))$
5	4	cbviotadavw	$⊢ φ \to (ι x \| (x \in A \land ψ)) = (ι y \| (y \in A \land χ))$
6		df-riota	$⊢ (ι x \in A \| ψ) = (ι x \| (x \in A \land ψ))$
7		df-riota	$⊢ (ι y \in A \| χ) = (ι y \| (y \in A \land χ))$
8	5 6 7	3eqtr4g	$⊢ φ \to (ι x \in A \| ψ) = (ι y \in A \| χ)$

Metamath Proof Explorer