Metamath Proof Explorer

Theorem funmpt3

Description: A function in maps-to notation with three arguments is a function. (Contributed by BTernaryTau, 8-Sep-2026)

		Ref	Expression
	Assertion	funmpt3	$⊢ Fun (x \in A, y \in B, z \in C ⟼ D)$

Proof

Step	Hyp	Ref	Expression
1		funopab	$⊢ Fun \{⟨v, w⟩ \| \exists x \in A \exists y \in B \exists z \in C (v = ⟨x, y, z⟩ \land w = D)\} \leftrightarrow \forall v \exists^{*} w \exists x \in A \exists y \in B \exists z \in C (v = ⟨x, y, z⟩ \land w = D)$
2		moeq	$⊢ \exists^{*} w w = D$
3	2	moani	$⊢ \exists^{*} w ((x \in A \land y \in B \land z \in C) \land w = D)$
4	3	ax-gen	$⊢ \forall z \exists^{*} w ((x \in A \land y \in B \land z \in C) \land w = D)$
5	4	gen2	$⊢ \forall x \forall y \forall z \exists^{*} w ((x \in A \land y \in B \land z \in C) \land w = D)$
6		mosubott	$⊢ \forall x \forall y \forall z \exists^{} w ((x \in A \land y \in B \land z \in C) \land w = D) \to \exists^{} w \exists x \exists y \exists z (v = ⟨x, y, z⟩ \land ((x \in A \land y \in B \land z \in C) \land w = D))$
7	5 6	ax-mp	$⊢ \exists^{*} w \exists x \exists y \exists z (v = ⟨x, y, z⟩ \land ((x \in A \land y \in B \land z \in C) \land w = D))$
8		r3ex	$⊢ \exists x \in A \exists y \in B \exists z \in C (v = ⟨x, y, z⟩ \land w = D) \leftrightarrow \exists x \exists y \exists z ((x \in A \land y \in B \land z \in C) \land (v = ⟨x, y, z⟩ \land w = D))$
9		an12	$⊢ (v = ⟨x, y, z⟩ \land ((x \in A \land y \in B \land z \in C) \land w = D)) \leftrightarrow ((x \in A \land y \in B \land z \in C) \land (v = ⟨x, y, z⟩ \land w = D))$
10	9	3exbii	$⊢ \exists x \exists y \exists z (v = ⟨x, y, z⟩ \land ((x \in A \land y \in B \land z \in C) \land w = D)) \leftrightarrow \exists x \exists y \exists z ((x \in A \land y \in B \land z \in C) \land (v = ⟨x, y, z⟩ \land w = D))$
11	8 10	bitr4i	$⊢ \exists x \in A \exists y \in B \exists z \in C (v = ⟨x, y, z⟩ \land w = D) \leftrightarrow \exists x \exists y \exists z (v = ⟨x, y, z⟩ \land ((x \in A \land y \in B \land z \in C) \land w = D))$
12	11	mobii	$⊢ \exists^{} w \exists x \in A \exists y \in B \exists z \in C (v = ⟨x, y, z⟩ \land w = D) \leftrightarrow \exists^{} w \exists x \exists y \exists z (v = ⟨x, y, z⟩ \land ((x \in A \land y \in B \land z \in C) \land w = D))$
13	7 12	mpbir	$⊢ \exists^{*} w \exists x \in A \exists y \in B \exists z \in C (v = ⟨x, y, z⟩ \land w = D)$
14	1 13	mpgbir	$⊢ Fun \{⟨v, w⟩ \| \exists x \in A \exists y \in B \exists z \in C (v = ⟨x, y, z⟩ \land w = D)\}$
15		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)\}$
16	15	funeqi	$⊢ Fun (x \in A, y \in B, z \in C ⟼ D) \leftrightarrow Fun \{⟨v, w⟩ \| \exists x \in A \exists y \in B \exists z \in C (v = ⟨x, y, z⟩ \land w = D)\}$
17	14 16	mpbir	$⊢ Fun (x \in A, y \in B, z \in C ⟼ D)$