cbvriotavw

Description: Change bound variable in a restricted description binder. Version of cbvriotav with a disjoint variable condition, which requires fewer axioms . (Contributed by NM, 18-Mar-2013) (Revised by Gino Giotto, 30-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		cbvriotavw.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
2		eleq1w	$⊢ x = y \to (x \in A \leftrightarrow y \in A)$
3	2 1	anbi12d	$⊢ x = y \to ((x \in A \land φ) \leftrightarrow (y \in A \land ψ))$
4	3	cbviotavw	$⊢ (ι x \| (x \in A \land φ)) = (ι y \| (y \in A \land ψ))$
5		df-riota	$⊢ (ι x \in A \| φ) = (ι x \| (x \in A \land φ))$
6		df-riota	$⊢ (ι y \in A \| ψ) = (ι y \| (y \in A \land ψ))$
7	4 5 6	3eqtr4i	$⊢ (ι x \in A \| φ) = (ι y \in A \| ψ)$

Metamath Proof Explorer

Theorem cbvriotavw

Proof