mpofvd

Description: Value of a two-argument function (usually an operation) in maps-to notation. (Contributed by BTernaryTau, 18-Oct-2026)

	Ref	Expression
Hypotheses	mpofvd.1	$⊢ φ \to X \in (A \times B)$
	mpofvd.2	$⊢ φ \to Y \in V$
	mpofvd.3	$⊢ (φ \land X = ⟨x, y⟩) \to Y = C$
	mpofvd.4	$⊢ F = (x \in A, y \in B ⟼ C)$
Assertion	mpofvd	$⊢ φ \to F (X) = Y$

Proof

Step	Hyp	Ref	Expression
1		mpofvd.1	$⊢ φ \to X \in (A \times B)$
2		mpofvd.2	$⊢ φ \to Y \in V$
3		mpofvd.3	$⊢ (φ \land X = ⟨x, y⟩) \to Y = C$
4		mpofvd.4	$⊢ F = (x \in A, y \in B ⟼ C)$
5		elxpi	$⊢ X \in (A \times B) \to \exists x \exists y (X = ⟨x, y⟩ \land (x \in A \land y \in B))$
6	1 5	syl	$⊢ φ \to \exists x \exists y (X = ⟨x, y⟩ \land (x \in A \land y \in B))$
7		idd	$⊢ (φ \land X = ⟨x, y⟩) \to ((x \in A \land y \in B) \to (x \in A \land y \in B))$
8	7 3	jctird	$⊢ (φ \land X = ⟨x, y⟩) \to ((x \in A \land y \in B) \to ((x \in A \land y \in B) \land Y = C))$
9	8	imdistanda	$⊢ φ \to ((X = ⟨x, y⟩ \land (x \in A \land y \in B)) \to (X = ⟨x, y⟩ \land ((x \in A \land y \in B) \land Y = C)))$
10	9	2eximdv	$⊢ φ \to (\exists x \exists y (X = ⟨x, y⟩ \land (x \in A \land y \in B)) \to \exists x \exists y (X = ⟨x, y⟩ \land ((x \in A \land y \in B) \land Y = C)))$
11	6 10	mpd	$⊢ φ \to \exists x \exists y (X = ⟨x, y⟩ \land ((x \in A \land y \in B) \land Y = C))$
12	1	elexd	$⊢ φ \to X \in V$
13		eqeq1	$⊢ w = X \to (w = ⟨x, y⟩ \leftrightarrow X = ⟨x, y⟩)$
14	13	anbi1d	$⊢ w = X \to ((w = ⟨x, y⟩ \land ((x \in A \land y \in B) \land z = C)) \leftrightarrow (X = ⟨x, y⟩ \land ((x \in A \land y \in B) \land z = C)))$
15	14	2exbidv	$⊢ w = X \to (\exists x \exists y (w = ⟨x, y⟩ \land ((x \in A \land y \in B) \land z = C)) \leftrightarrow \exists x \exists y (X = ⟨x, y⟩ \land ((x \in A \land y \in B) \land z = C)))$
16		eqeq1	$⊢ z = Y \to (z = C \leftrightarrow Y = C)$
17	16	anbi2d	$⊢ z = Y \to (((x \in A \land y \in B) \land z = C) \leftrightarrow ((x \in A \land y \in B) \land Y = C))$
18	17	anbi2d	$⊢ z = Y \to ((X = ⟨x, y⟩ \land ((x \in A \land y \in B) \land z = C)) \leftrightarrow (X = ⟨x, y⟩ \land ((x \in A \land y \in B) \land Y = C)))$
19	18	2exbidv	$⊢ z = Y \to (\exists x \exists y (X = ⟨x, y⟩ \land ((x \in A \land y \in B) \land z = C)) \leftrightarrow \exists x \exists y (X = ⟨x, y⟩ \land ((x \in A \land y \in B) \land Y = C)))$
20		moeq	$⊢ \exists^{*} z z = C$
21	20	moani	$⊢ \exists^{*} z ((x \in A \land y \in B) \land z = C)$
22	21	mosubop	$⊢ \exists^{*} z \exists x \exists y (w = ⟨x, y⟩ \land ((x \in A \land y \in B) \land z = C))$
23	22	a1i	$⊢ w \in V \to \exists^{*} z \exists x \exists y (w = ⟨x, y⟩ \land ((x \in A \land y \in B) \land z = C))$
24		df-mpo	$⊢ (x \in A, y \in B ⟼ C) = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\}$
25		dfoprab2	$⊢ \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\} = \{⟨w, z⟩ \| \exists x \exists y (w = ⟨x, y⟩ \land ((x \in A \land y \in B) \land z = C))\}$
26	4 24 25	3eqtri	$⊢ F = \{⟨w, z⟩ \| \exists x \exists y (w = ⟨x, y⟩ \land ((x \in A \land y \in B) \land z = C))\}$
27		vex	$⊢ w \in V$
28	27	biantrur	$⊢ \exists x \exists y (w = ⟨x, y⟩ \land ((x \in A \land y \in B) \land z = C)) \leftrightarrow (w \in V \land \exists x \exists y (w = ⟨x, y⟩ \land ((x \in A \land y \in B) \land z = C)))$
29	28	opabbii	$⊢ \{⟨w, z⟩ \| \exists x \exists y (w = ⟨x, y⟩ \land ((x \in A \land y \in B) \land z = C))\} = \{⟨w, z⟩ \| (w \in V \land \exists x \exists y (w = ⟨x, y⟩ \land ((x \in A \land y \in B) \land z = C)))\}$
30	26 29	eqtri	$⊢ F = \{⟨w, z⟩ \| (w \in V \land \exists x \exists y (w = ⟨x, y⟩ \land ((x \in A \land y \in B) \land z = C)))\}$
31	15 19 23 30	fvopab3ig	$⊢ (X \in V \land Y \in V) \to (\exists x \exists y (X = ⟨x, y⟩ \land ((x \in A \land y \in B) \land Y = C)) \to F (X) = Y)$
32	12 2 31	syl2anc	$⊢ φ \to (\exists x \exists y (X = ⟨x, y⟩ \land ((x \in A \land y \in B) \land Y = C)) \to F (X) = Y)$
33	11 32	mpd	$⊢ φ \to F (X) = Y$

Metamath Proof Explorer

Theorem mpofvd

Proof