cbvmptv

Description: Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by Mario Carneiro, 19-Feb-2013) Add disjoint variable condition to avoid auxiliary axioms . See cbvmptvg for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 17-Nov-2024)

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

Proof

Step	Hyp	Ref	Expression
1		cbvmptv.1	$⊢ x = y \to B = C$
2		eleq1w	$⊢ x = y \to (x \in A \leftrightarrow y \in A)$
3	1	eqeq2d	$⊢ x = y \to (z = B \leftrightarrow z = C)$
4	2 3	anbi12d	$⊢ x = y \to ((x \in A \land z = B) \leftrightarrow (y \in A \land z = C))$
5	4	cbvopab1v	$⊢ \{⟨x, z⟩ \| (x \in A \land z = B)\} = \{⟨y, z⟩ \| (y \in A \land z = C)\}$
6		df-mpt	$⊢ (x \in A ⟼ B) = \{⟨x, z⟩ \| (x \in A \land z = B)\}$
7		df-mpt	$⊢ (y \in A ⟼ C) = \{⟨y, z⟩ \| (y \in A \land z = C)\}$
8	5 6 7	3eqtr4i	$⊢ (x \in A ⟼ B) = (y \in A ⟼ C)$

Metamath Proof Explorer

Theorem cbvmptv

Proof