aovmpt4g

Description: Value of a function given by the maps-to notation, analogous to ovmpt4g . (Contributed by Alexander van der Vekens, 26-May-2017)

		Ref	Expression
	Hypothesis	aovmpt4g.3	$⊢ F = (x \in A, y \in B ⟼ C)$
	Assertion	aovmpt4g	$⊢ (x \in A \land y \in B \land C \in V) \to ((x F y)) = C$

Step	Hyp	Ref	Expression
1		aovmpt4g.3	$⊢ F = (x \in A, y \in B ⟼ C)$
2	1	dmmpog	$⊢ C \in V \to dom F = A \times B$
3		opelxpi	$⊢ (x \in A \land y \in B) \to ⟨x, y⟩ \in (A \times B)$
4		eleq2	$⊢ dom F = A \times B \to (⟨x, y⟩ \in dom F \leftrightarrow ⟨x, y⟩ \in (A \times B))$
5	3 4	imbitrrid	$⊢ dom F = A \times B \to ((x \in A \land y \in B) \to ⟨x, y⟩ \in dom F)$
6	2 5	syl	$⊢ C \in V \to ((x \in A \land y \in B) \to ⟨x, y⟩ \in dom F)$
7	6	impcom	$⊢ ((x \in A \land y \in B) \land C \in V) \to ⟨x, y⟩ \in dom F$
8	7	3impa	$⊢ (x \in A \land y \in B \land C \in V) \to ⟨x, y⟩ \in dom F$
9	1	mpofun	$⊢ Fun F$
10		funres	$⊢ Fun F \to Fun ({F ↾}_{\{⟨x, y⟩\}})$
11	9 10	ax-mp	$⊢ Fun ({F ↾}_{\{⟨x, y⟩\}})$
12		df-dfat	$⊢ F defAt ⟨x, y⟩ \leftrightarrow (⟨x, y⟩ \in dom F \land Fun ({F ↾}_{\{⟨x, y⟩\}}))$
13		aovfundmoveq	$⊢ F defAt ⟨x, y⟩ \to ((x F y)) = x F y$
14	12 13	sylbir	$⊢ (⟨x, y⟩ \in dom F \land Fun ({F ↾}_{\{⟨x, y⟩\}})) \to ((x F y)) = x F y$
15	8 11 14	sylancl	$⊢ (x \in A \land y \in B \land C \in V) \to ((x F y)) = x F y$
16	1	ovmpt4g	$⊢ (x \in A \land y \in B \land C \in V) \to x F y = C$
17	15 16	eqtrd	$⊢ (x \in A \land y \in B \land C \in V) \to ((x F y)) = C$

Metamath Proof Explorer