mpt3eqdv

Description: An equality deduction for maps-to notation. (Contributed by BTernaryTau, 8-Sep-2026)

	Ref	Expression
Hypotheses	mpt3eqdv.1	$⊢ φ \to A = E$
	mpt3eqdv.2	$⊢ φ \to B = F$
	mpt3eqdv.3	$⊢ φ \to C = G$
	mpt3eqdv.4	$⊢ (φ \land (x \in A \land y \in B \land z \in C)) \to D = H$
Assertion	mpt3eqdv	$⊢ φ \to (x \in A, y \in B, z \in C ⟼ D) = (x \in E, y \in F, z \in G ⟼ H)$

Proof

Step	Hyp	Ref	Expression
1		mpt3eqdv.1	$⊢ φ \to A = E$
2		mpt3eqdv.2	$⊢ φ \to B = F$
3		mpt3eqdv.3	$⊢ φ \to C = G$
4		mpt3eqdv.4	$⊢ (φ \land (x \in A \land y \in B \land z \in C)) \to D = H$
5	2	adantr	$⊢ (φ \land x \in A) \to B = F$
6	3	3ad2ant1	$⊢ (φ \land x \in A \land y \in B) \to C = G$
7		3an4anass	$⊢ ((φ \land x \in A \land y \in B) \land z \in C) \leftrightarrow ((φ \land x \in A) \land (y \in B \land z \in C))$
8		13an22anass	$⊢ (φ \land (x \in A \land y \in B \land z \in C)) \leftrightarrow ((φ \land x \in A) \land (y \in B \land z \in C))$
9	7 8	bitr4i	$⊢ ((φ \land x \in A \land y \in B) \land z \in C) \leftrightarrow (φ \land (x \in A \land y \in B \land z \in C))$
10	4	eqeq2d	$⊢ (φ \land (x \in A \land y \in B \land z \in C)) \to (w = D \leftrightarrow w = H)$
11	10	anbi2d	$⊢ (φ \land (x \in A \land y \in B \land z \in C)) \to ((v = ⟨x, y, z⟩ \land w = D) \leftrightarrow (v = ⟨x, y, z⟩ \land w = H))$
12	9 11	sylbi	$⊢ ((φ \land x \in A \land y \in B) \land z \in C) \to ((v = ⟨x, y, z⟩ \land w = D) \leftrightarrow (v = ⟨x, y, z⟩ \land w = H))$
13	6 12	rexeqbidva	$⊢ (φ \land x \in A \land y \in B) \to (\exists z \in C (v = ⟨x, y, z⟩ \land w = D) \leftrightarrow \exists z \in G (v = ⟨x, y, z⟩ \land w = H))$
14	13	3expa	$⊢ ((φ \land x \in A) \land y \in B) \to (\exists z \in C (v = ⟨x, y, z⟩ \land w = D) \leftrightarrow \exists z \in G (v = ⟨x, y, z⟩ \land w = H))$
15	5 14	rexeqbidva	$⊢ (φ \land x \in A) \to (\exists y \in B \exists z \in C (v = ⟨x, y, z⟩ \land w = D) \leftrightarrow \exists y \in F \exists z \in G (v = ⟨x, y, z⟩ \land w = H))$
16	1 15	rexeqbidva	$⊢ φ \to (\exists x \in A \exists y \in B \exists z \in C (v = ⟨x, y, z⟩ \land w = D) \leftrightarrow \exists x \in E \exists y \in F \exists z \in G (v = ⟨x, y, z⟩ \land w = H))$
17	16	opabbidv	$⊢ φ \to \{⟨v, w⟩ \| \exists x \in A \exists y \in B \exists z \in C (v = ⟨x, y, z⟩ \land w = D)\} = \{⟨v, w⟩ \| \exists x \in E \exists y \in F \exists z \in G (v = ⟨x, y, z⟩ \land w = H)\}$
18		df-mpt3	$⊢ (x \in A, y \in B, z \in C ⟼ D) = \{⟨v, w⟩ \| \exists x \in A \exists y \in B \exists z \in C (v = ⟨x, y, z⟩ \land w = D)\}$
19		df-mpt3	$⊢ (x \in E, y \in F, z \in G ⟼ H) = \{⟨v, w⟩ \| \exists x \in E \exists y \in F \exists z \in G (v = ⟨x, y, z⟩ \land w = H)\}$
20	17 18 19	3eqtr4g	$⊢ φ \to (x \in A, y \in B, z \in C ⟼ D) = (x \in E, y \in F, z \in G ⟼ H)$

Metamath Proof Explorer

Theorem mpt3eqdv

Proof