This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cbvmpov

Description: Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt , some distinct variable requirements could be eliminated. (Contributed by NM, 11-Jun-2013)

		Ref	Expression
	Hypotheses	cbvmpov.1	$⊢ x = z \to C = E$
		cbvmpov.2	$⊢ y = w \to E = D$
	Assertion	cbvmpov	$⊢ (x \in A, y \in B ⟼ C) = (z \in A, w \in B ⟼ D)$

Proof

Step	Hyp	Ref	Expression
1		cbvmpov.1	$⊢ x = z \to C = E$
2		cbvmpov.2	$⊢ y = w \to E = D$
3		eleq1w	$⊢ x = z \to (x \in A \leftrightarrow z \in A)$
4		eleq1w	$⊢ y = w \to (y \in B \leftrightarrow w \in B)$
5	3 4	bi2anan9	$⊢ (x = z \land y = w) \to ((x \in A \land y \in B) \leftrightarrow (z \in A \land w \in B))$
6	1 2	sylan9eq	$⊢ (x = z \land y = w) \to C = D$
7	6	eqeq2d	$⊢ (x = z \land y = w) \to (v = C \leftrightarrow v = D)$
8	5 7	anbi12d	$⊢ (x = z \land y = w) \to (((x \in A \land y \in B) \land v = C) \leftrightarrow ((z \in A \land w \in B) \land v = D))$
9	8	cbvoprab12v	$⊢ \{⟨⟨x, y⟩, v⟩ \| ((x \in A \land y \in B) \land v = C)\} = \{⟨⟨z, w⟩, v⟩ \| ((z \in A \land w \in B) \land v = D)\}$
10		df-mpo	$⊢ (x \in A, y \in B ⟼ C) = \{⟨⟨x, y⟩, v⟩ \| ((x \in A \land y \in B) \land v = C)\}$
11		df-mpo	$⊢ (z \in A, w \in B ⟼ D) = \{⟨⟨z, w⟩, v⟩ \| ((z \in A \land w \in B) \land v = D)\}$
12	9 10 11	3eqtr4i	$⊢ (x \in A, y \in B ⟼ C) = (z \in A, w \in B ⟼ D)$