cbvmpodavw2

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

Step	Hyp	Ref	Expression
1		cbvmpodavw2.1	$⊢ ((φ \land x = z) \land y = w) \to E = F$
2		cbvmpodavw2.2	$⊢ ((φ \land x = z) \land y = w) \to C = D$
3		cbvmpodavw2.3	$⊢ ((φ \land x = z) \land y = w) \to A = B$
4		simplr	$⊢ ((φ \land x = z) \land y = w) \to x = z$
5	4 3	eleq12d	$⊢ ((φ \land x = z) \land y = w) \to (x \in A \leftrightarrow z \in B)$
6		simpr	$⊢ ((φ \land x = z) \land y = w) \to y = w$
7	6 2	eleq12d	$⊢ ((φ \land x = z) \land y = w) \to (y \in C \leftrightarrow w \in D)$
8	5 7	anbi12d	$⊢ ((φ \land x = z) \land y = w) \to ((x \in A \land y \in C) \leftrightarrow (z \in B \land w \in D))$
9	1	eqeq2d	$⊢ ((φ \land x = z) \land y = w) \to (t = E \leftrightarrow t = F)$
10	8 9	anbi12d	$⊢ ((φ \land x = z) \land y = w) \to (((x \in A \land y \in C) \land t = E) \leftrightarrow ((z \in B \land w \in D) \land t = F))$
11	10	cbvoprab12davw	$⊢ φ \to \{⟨⟨x, y⟩, t⟩ \| ((x \in A \land y \in C) \land t = E)\} = \{⟨⟨z, w⟩, t⟩ \| ((z \in B \land w \in D) \land t = F)\}$
12		df-mpo	$⊢ (x \in A, y \in C ⟼ E) = \{⟨⟨x, y⟩, t⟩ \| ((x \in A \land y \in C) \land t = E)\}$
13		df-mpo	$⊢ (z \in B, w \in D ⟼ F) = \{⟨⟨z, w⟩, t⟩ \| ((z \in B \land w \in D) \land t = F)\}$
14	11 12 13	3eqtr4g	$⊢ φ \to (x \in A, y \in C ⟼ E) = (z \in B, w \in D ⟼ F)$

Metamath Proof Explorer