Metamath Proof Explorer

Theorem mpt3mpt

Description: Express a three-argument function as a one-argument function, or vice-versa. (Contributed by BTernaryTau, 7-Sep-2026)

		Ref	Expression
	Hypothesis	mpt3mpt.1	$⊢ w = ⟨x, y, z⟩ \to D = E$
	Assertion	mpt3mpt	$⊢ (w \in ((A \times B) \times C) ⟼ D) = (x \in A, y \in B, z \in C ⟼ E)$

Proof

Step	Hyp	Ref	Expression
1		mpt3mpt.1	$⊢ w = ⟨x, y, z⟩ \to D = E$
2		el2xptp	$⊢ w \in ((A \times B) \times C) \leftrightarrow \exists x \in A \exists y \in B \exists z \in C w = ⟨x, y, z⟩$
3	2	anbi1i	$⊢ (w \in ((A \times B) \times C) \land t = D) \leftrightarrow (\exists x \in A \exists y \in B \exists z \in C w = ⟨x, y, z⟩ \land t = D)$
4		r19.41v	$⊢ \exists x \in A (\exists y \in B \exists z \in C w = ⟨x, y, z⟩ \land t = D) \leftrightarrow (\exists x \in A \exists y \in B \exists z \in C w = ⟨x, y, z⟩ \land t = D)$
5		r19.41v	$⊢ \exists y \in B (\exists z \in C w = ⟨x, y, z⟩ \land t = D) \leftrightarrow (\exists y \in B \exists z \in C w = ⟨x, y, z⟩ \land t = D)$
6		r19.41v	$⊢ \exists z \in C (w = ⟨x, y, z⟩ \land t = D) \leftrightarrow (\exists z \in C w = ⟨x, y, z⟩ \land t = D)$
7	1	eqeq2d	$⊢ w = ⟨x, y, z⟩ \to (t = D \leftrightarrow t = E)$
8	7	pm5.32i	$⊢ (w = ⟨x, y, z⟩ \land t = D) \leftrightarrow (w = ⟨x, y, z⟩ \land t = E)$
9	8	rexbii	$⊢ \exists z \in C (w = ⟨x, y, z⟩ \land t = D) \leftrightarrow \exists z \in C (w = ⟨x, y, z⟩ \land t = E)$
10	6 9	bitr3i	$⊢ (\exists z \in C w = ⟨x, y, z⟩ \land t = D) \leftrightarrow \exists z \in C (w = ⟨x, y, z⟩ \land t = E)$
11	10	rexbii	$⊢ \exists y \in B (\exists z \in C w = ⟨x, y, z⟩ \land t = D) \leftrightarrow \exists y \in B \exists z \in C (w = ⟨x, y, z⟩ \land t = E)$
12	5 11	bitr3i	$⊢ (\exists y \in B \exists z \in C w = ⟨x, y, z⟩ \land t = D) \leftrightarrow \exists y \in B \exists z \in C (w = ⟨x, y, z⟩ \land t = E)$
13	12	rexbii	$⊢ \exists x \in A (\exists y \in B \exists z \in C w = ⟨x, y, z⟩ \land t = D) \leftrightarrow \exists x \in A \exists y \in B \exists z \in C (w = ⟨x, y, z⟩ \land t = E)$
14	3 4 13	3bitr2i	$⊢ (w \in ((A \times B) \times C) \land t = D) \leftrightarrow \exists x \in A \exists y \in B \exists z \in C (w = ⟨x, y, z⟩ \land t = E)$
15	14	opabbii	$⊢ \{⟨w, t⟩ \| (w \in ((A \times B) \times C) \land t = D)\} = \{⟨w, t⟩ \| \exists x \in A \exists y \in B \exists z \in C (w = ⟨x, y, z⟩ \land t = E)\}$
16		df-mpt	$⊢ (w \in ((A \times B) \times C) ⟼ D) = \{⟨w, t⟩ \| (w \in ((A \times B) \times C) \land t = D)\}$
17		df-mpt3	$⊢ (x \in A, y \in B, z \in C ⟼ E) = \{⟨w, t⟩ \| \exists x \in A \exists y \in B \exists z \in C (w = ⟨x, y, z⟩ \land t = E)\}$
18	15 16 17	3eqtr4i	$⊢ (w \in ((A \times B) \times C) ⟼ D) = (x \in A, y \in B, z \in C ⟼ E)$