cbvmptdavw

Description: Change bound variable in a maps-to function. Deduction form. (Contributed by GG, 14-Aug-2025)

		Ref	Expression
	Hypothesis	cbvmptdavw.1	$⊢ (φ \land x = y) \to B = C$
	Assertion	cbvmptdavw	$⊢ φ \to (x \in A ⟼ B) = (y \in A ⟼ C)$

Step	Hyp	Ref	Expression
1		cbvmptdavw.1	$⊢ (φ \land x = y) \to B = C$
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	1	eqeq2d	$⊢ (φ \land x = y) \to (t = B \leftrightarrow t = C)$
5	3 4	anbi12d	$⊢ (φ \land x = y) \to ((x \in A \land t = B) \leftrightarrow (y \in A \land t = C))$
6	5	cbvopab1davw	$⊢ φ \to \{⟨x, t⟩ \| (x \in A \land t = B)\} = \{⟨y, t⟩ \| (y \in A \land t = C)\}$
7		df-mpt	$⊢ (x \in A ⟼ B) = \{⟨x, t⟩ \| (x \in A \land t = B)\}$
8		df-mpt	$⊢ (y \in A ⟼ C) = \{⟨y, t⟩ \| (y \in A \land t = C)\}$
9	6 7 8	3eqtr4g	$⊢ φ \to (x \in A ⟼ B) = (y \in A ⟼ C)$

Metamath Proof Explorer