Theorem ovmpt4g

Description: Value of a function given by the maps-to notation. (This is the operation analogue of fvmpt2 .) (Contributed by NM, 21-Feb-2004) (Revised by Mario Carneiro, 1-Sep-2015)

	Ref	Expression
Hypothesis	ovmpt4g.3	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
Assertion	ovmpt4g	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ) → ( 𝑥 𝐹 𝑦 ) = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		ovmpt4g.3	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
2		elisset	⊢ ( 𝐶 ∈ 𝑉 → ∃ 𝑧 𝑧 = 𝐶 )
3		moeq	⊢ ∃* 𝑧 𝑧 = 𝐶
4	3	a1i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ∃* 𝑧 𝑧 = 𝐶 )
5		df-mpo	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) }
6	1 5	eqtri	⊢ 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) }
7	4 6	ovidi	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑧 = 𝐶 → ( 𝑥 𝐹 𝑦 ) = 𝑧 ) )
8		eqeq2	⊢ ( 𝑧 = 𝐶 → ( ( 𝑥 𝐹 𝑦 ) = 𝑧 ↔ ( 𝑥 𝐹 𝑦 ) = 𝐶 ) )
9	7 8	mpbidi	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑧 = 𝐶 → ( 𝑥 𝐹 𝑦 ) = 𝐶 ) )
10	9	exlimdv	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( ∃ 𝑧 𝑧 = 𝐶 → ( 𝑥 𝐹 𝑦 ) = 𝐶 ) )
11	2 10	syl5	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝐶 ∈ 𝑉 → ( 𝑥 𝐹 𝑦 ) = 𝐶 ) )
12	11	3impia	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝑉 ) → ( 𝑥 𝐹 𝑦 ) = 𝐶 )