elovmpoeq

Description: If a value of an operation given by maps-to notation has a member, it equals the substituted body. (Contributed by Zhi Wang, 17-Sep-2026)

	Ref	Expression
Hypotheses	elovmpoeq.f	$⊢ F = (x \in A, y \in B ⟼ C)$
	elovmpoeq.s	$⊢ (x = X \land y = Y) \to C = D$
Assertion	elovmpoeq	$⊢ N \in (X F Y) \to X F Y = D$

Proof

Step	Hyp	Ref	Expression
1		elovmpoeq.f	$⊢ F = (x \in A, y \in B ⟼ C)$
2		elovmpoeq.s	$⊢ (x = X \land y = Y) \to C = D$
3		ne0i	$⊢ N \in (X F Y) \to X F Y \neq \emptyset$
4		df-ov	$⊢ X F Y = F (⟨X, Y⟩)$
5	4	eqcomi	$⊢ F (⟨X, Y⟩) = X F Y$
6		tz6.12i	$⊢ X F Y \neq \emptyset \to (F (⟨X, Y⟩) = X F Y \to ⟨X, Y⟩ F (X F Y))$
7	3 5 6	mpisyl	$⊢ N \in (X F Y) \to ⟨X, Y⟩ F (X F Y)$
8		df-br	$⊢ ⟨X, Y⟩ F (X F Y) \leftrightarrow ⟨⟨X, Y⟩, X F Y⟩ \in F$
9	7 8	sylib	$⊢ N \in (X F Y) \to ⟨⟨X, Y⟩, X F Y⟩ \in F$
10		df-mpo	$⊢ (x \in A, y \in B ⟼ C) = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\}$
11	1 10	eqtri	$⊢ F = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\}$
12	9 11	eleqtrdi	$⊢ N \in (X F Y) \to ⟨⟨X, Y⟩, X F Y⟩ \in \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\}$
13	1	elmpocl1	$⊢ N \in (X F Y) \to X \in A$
14	13	elexd	$⊢ N \in (X F Y) \to X \in V$
15	1	elmpocl2	$⊢ N \in (X F Y) \to Y \in B$
16	15	elexd	$⊢ N \in (X F Y) \to Y \in V$
17		ovexd	$⊢ N \in (X F Y) \to X F Y \in V$
18		simp1	$⊢ (x = X \land y = Y \land z = X F Y) \to x = X$
19	18	eleq1d	$⊢ (x = X \land y = Y \land z = X F Y) \to (x \in A \leftrightarrow X \in A)$
20		simp2	$⊢ (x = X \land y = Y \land z = X F Y) \to y = Y$
21	20	eleq1d	$⊢ (x = X \land y = Y \land z = X F Y) \to (y \in B \leftrightarrow Y \in B)$
22	19 21	anbi12d	$⊢ (x = X \land y = Y \land z = X F Y) \to ((x \in A \land y \in B) \leftrightarrow (X \in A \land Y \in B))$
23		simp3	$⊢ (x = X \land y = Y \land z = X F Y) \to z = X F Y$
24	2	3adant3	$⊢ (x = X \land y = Y \land z = X F Y) \to C = D$
25	23 24	eqeq12d	$⊢ (x = X \land y = Y \land z = X F Y) \to (z = C \leftrightarrow X F Y = D)$
26	22 25	anbi12d	$⊢ (x = X \land y = Y \land z = X F Y) \to (((x \in A \land y \in B) \land z = C) \leftrightarrow ((X \in A \land Y \in B) \land X F Y = D))$
27	26	eloprabga	$⊢ (X \in V \land Y \in V \land X F Y \in V) \to (⟨⟨X, Y⟩, X F Y⟩ \in \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\} \leftrightarrow ((X \in A \land Y \in B) \land X F Y = D))$
28	14 16 17 27	syl3anc	$⊢ N \in (X F Y) \to (⟨⟨X, Y⟩, X F Y⟩ \in \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\} \leftrightarrow ((X \in A \land Y \in B) \land X F Y = D))$
29	12 28	mpbid	$⊢ N \in (X F Y) \to ((X \in A \land Y \in B) \land X F Y = D)$
30	29	simprd	$⊢ N \in (X F Y) \to X F Y = D$

Metamath Proof Explorer

Theorem elovmpoeq

Proof