Theorem elovmpoeq 50071

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.)

Hypotheses

Ref	Expression
elovmpoeq.f	⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
elovmpoeq.s	⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → 𝐶 = 𝐷)

Assertion

Ref	Expression
elovmpoeq	⊢ (𝑁 ∈ (𝑋𝐹𝑌) → (𝑋𝐹𝑌) = 𝐷)

Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦   𝑥,𝐷,𝑦   𝑥,𝐹,𝑦   𝑥,𝑋,𝑦   𝑥,𝑌,𝑦

Allowed substitution hints:   𝐶(𝑥, 𝑦)   𝑁(𝑥, 𝑦)

Proof of Theorem elovmpoeq

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ne0i 4286	. . . . . 6 ⊢ (𝑁 ∈ (𝑋𝐹𝑌) → (𝑋𝐹𝑌) ≠ ∅)
2		df-ov 7423	. . . . . . 7 ⊢ (𝑋𝐹𝑌) = (𝐹‘⟨𝑋, 𝑌⟩)
3	2	eqcomi 2769	. . . . . 6 ⊢ (𝐹‘⟨𝑋, 𝑌⟩) = (𝑋𝐹𝑌)
4		tz6.12i 6911	. . . . . 6 ⊢ ((𝑋𝐹𝑌) ≠ ∅ → ((𝐹‘⟨𝑋, 𝑌⟩) = (𝑋𝐹𝑌) → ⟨𝑋, 𝑌⟩𝐹(𝑋𝐹𝑌)))
5	1, 3, 4	mpisyl 22	. . . . 5 ⊢ (𝑁 ∈ (𝑋𝐹𝑌) → ⟨𝑋, 𝑌⟩𝐹(𝑋𝐹𝑌))
6		df-br 5103	. . . . 5 ⊢ (⟨𝑋, 𝑌⟩𝐹(𝑋𝐹𝑌) ↔ ⟨⟨𝑋, 𝑌⟩, (𝑋𝐹𝑌)⟩ ∈ 𝐹)
7	5, 6	sylib 221	. . . 4 ⊢ (𝑁 ∈ (𝑋𝐹𝑌) → ⟨⟨𝑋, 𝑌⟩, (𝑋𝐹𝑌)⟩ ∈ 𝐹)
8		elovmpoeq.f	. . . . 5 ⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
9		df-mpo 7425	. . . . 5 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
10	8, 9	eqtri 2783	. . . 4 ⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
11	7, 10	eleqtrdi 2870	. . 3 ⊢ (𝑁 ∈ (𝑋𝐹𝑌) → ⟨⟨𝑋, 𝑌⟩, (𝑋𝐹𝑌)⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)})
12	8	elmpocl1 7663	. . . . 5 ⊢ (𝑁 ∈ (𝑋𝐹𝑌) → 𝑋 ∈ 𝐴)
13	12	elexd 3473	. . . 4 ⊢ (𝑁 ∈ (𝑋𝐹𝑌) → 𝑋 ∈ V)
14	8	elmpocl2 7664	. . . . 5 ⊢ (𝑁 ∈ (𝑋𝐹𝑌) → 𝑌 ∈ 𝐵)
15	14	elexd 3473	. . . 4 ⊢ (𝑁 ∈ (𝑋𝐹𝑌) → 𝑌 ∈ V)
16		ovexd 7455	. . . 4 ⊢ (𝑁 ∈ (𝑋𝐹𝑌) → (𝑋𝐹𝑌) ∈ V)
17		simp1 1154	. . . . . . . 8 ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ∧ 𝑧 = (𝑋𝐹𝑌)) → 𝑥 = 𝑋)
18	17	eleq1d 2845	. . . . . . 7 ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ∧ 𝑧 = (𝑋𝐹𝑌)) → (𝑥 ∈ 𝐴 ↔ 𝑋 ∈ 𝐴))
19		simp2 1155	. . . . . . . 8 ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ∧ 𝑧 = (𝑋𝐹𝑌)) → 𝑦 = 𝑌)
20	19	eleq1d 2845	. . . . . . 7 ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ∧ 𝑧 = (𝑋𝐹𝑌)) → (𝑦 ∈ 𝐵 ↔ 𝑌 ∈ 𝐵))
21	18, 20	anbi12d 644	. . . . . 6 ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ∧ 𝑧 = (𝑋𝐹𝑌)) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵)))
22		simp3 1156	. . . . . . 7 ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ∧ 𝑧 = (𝑋𝐹𝑌)) → 𝑧 = (𝑋𝐹𝑌))
23		elovmpoeq.s	. . . . . . . 8 ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → 𝐶 = 𝐷)
24	23	3adant3 1150	. . . . . . 7 ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ∧ 𝑧 = (𝑋𝐹𝑌)) → 𝐶 = 𝐷)
25	22, 24	eqeq12d 2776	. . . . . 6 ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ∧ 𝑧 = (𝑋𝐹𝑌)) → (𝑧 = 𝐶 ↔ (𝑋𝐹𝑌) = 𝐷))
26	21, 25	anbi12d 644	. . . . 5 ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ∧ 𝑧 = (𝑋𝐹𝑌)) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋𝐹𝑌) = 𝐷)))
27	26	eloprabga 7529	. . . 4 ⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V ∧ (𝑋𝐹𝑌) ∈ V) → (⟨⟨𝑋, 𝑌⟩, (𝑋𝐹𝑌)⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} ↔ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋𝐹𝑌) = 𝐷)))
28	13, 15, 16, 27	syl3anc 1398	. . 3 ⊢ (𝑁 ∈ (𝑋𝐹𝑌) → (⟨⟨𝑋, 𝑌⟩, (𝑋𝐹𝑌)⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} ↔ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋𝐹𝑌) = 𝐷)))
29	11, 28	mpbid 235	. 2 ⊢ (𝑁 ∈ (𝑋𝐹𝑌) → ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋𝐹𝑌) = 𝐷))
30	29	simprd 501	1 ⊢ (𝑁 ∈ (𝑋𝐹𝑌) → (𝑋𝐹𝑌) = 𝐷)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144   ≠ wne 2955  Vcvv 3450  ∅c0 4278  ⟨cop 4589   class class class wbr 5102  ‘cfv 6538  (class class class)co 7420  {coprab 7421   ∈ cmpo 7422

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-xp 5656  df-dm 5660  df-iota 6494  df-fv 6546  df-ov 7423  df-oprab 7424  df-mpo 7425

This theorem is used by:  parhomvaln0  50844