Theorem 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	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 × 𝐵 ) )
	mpofvd.2	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
	mpofvd.3	⊢ ( ( 𝜑 ∧ 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑌 = 𝐶 )
	mpofvd.4	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
Assertion	mpofvd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		mpofvd.1	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 × 𝐵 ) )
2		mpofvd.2	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
3		mpofvd.3	⊢ ( ( 𝜑 ∧ 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑌 = 𝐶 )
4		mpofvd.4	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
5		elxpi	⊢ ( 𝑋 ∈ ( 𝐴 × 𝐵 ) → ∃ 𝑥 ∃ 𝑦 ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
6	1 5	syl	⊢ ( 𝜑 → ∃ 𝑥 ∃ 𝑦 ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
7		idd	⊢ ( ( 𝜑 ∧ 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
8	7 3	jctird	⊢ ( ( 𝜑 ∧ 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑌 = 𝐶 ) ) )
9	8	imdistanda	⊢ ( 𝜑 → ( ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑌 = 𝐶 ) ) ) )
10	9	2eximdv	⊢ ( 𝜑 → ( ∃ 𝑥 ∃ 𝑦 ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ∃ 𝑥 ∃ 𝑦 ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑌 = 𝐶 ) ) ) )
11	6 10	mpd	⊢ ( 𝜑 → ∃ 𝑥 ∃ 𝑦 ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑌 = 𝐶 ) ) )
12	1	elexd	⊢ ( 𝜑 → 𝑋 ∈ V )
13		eqeq1	⊢ ( 𝑤 = 𝑋 → ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ) )
14	13	anbi1d	⊢ ( 𝑤 = 𝑋 → ( ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ↔ ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ) )
15	14	2exbidv	⊢ ( 𝑤 = 𝑋 → ( ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ) )
16		eqeq1	⊢ ( 𝑧 = 𝑌 → ( 𝑧 = 𝐶 ↔ 𝑌 = 𝐶 ) )
17	16	anbi2d	⊢ ( 𝑧 = 𝑌 → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑌 = 𝐶 ) ) )
18	17	anbi2d	⊢ ( 𝑧 = 𝑌 → ( ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ↔ ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑌 = 𝐶 ) ) ) )
19	18	2exbidv	⊢ ( 𝑧 = 𝑌 → ( ∃ 𝑥 ∃ 𝑦 ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑌 = 𝐶 ) ) ) )
20		moeq	⊢ ∃* 𝑧 𝑧 = 𝐶
21	20	moani	⊢ ∃* 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 )
22	21	mosubop	⊢ ∃* 𝑧 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) )
23	22	a1i	⊢ ( 𝑤 ∈ V → ∃* 𝑧 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) )
24		df-mpo	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) }
25		dfoprab2	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) } = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) }
26	4 24 25	3eqtri	⊢ 𝐹 = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) }
27		vex	⊢ 𝑤 ∈ V
28	27	biantrur	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ↔ ( 𝑤 ∈ V ∧ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ) )
29	28	opabbii	⊢ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) } = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ V ∧ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ) }
30	26 29	eqtri	⊢ 𝐹 = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ V ∧ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ) }
31	15 19 23 30	fvopab3ig	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ 𝑉 ) → ( ∃ 𝑥 ∃ 𝑦 ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑌 = 𝐶 ) ) → ( 𝐹 ‘ 𝑋 ) = 𝑌 ) )
32	12 2 31	syl2anc	⊢ ( 𝜑 → ( ∃ 𝑥 ∃ 𝑦 ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑌 = 𝐶 ) ) → ( 𝐹 ‘ 𝑋 ) = 𝑌 ) )
33	11 32	mpd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = 𝑌 )