Metamath Proof Explorer

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	$⊢ F = (x \in A, y \in B ⟼ C)$
	Assertion	ovmpt4g	$⊢ (x \in A \land y \in B \land C \in V) \to x F y = C$

Proof

Step	Hyp	Ref	Expression
1		ovmpt4g.3	$⊢ F = (x \in A, y \in B ⟼ C)$
2		elisset	$⊢ C \in V \to \exists z z = C$
3		moeq	$⊢ \exists^{*} z z = C$
4	3	a1i	$⊢ (x \in A \land y \in B) \to \exists^{*} z z = C$
5		df-mpo	$⊢ (x \in A, y \in B ⟼ C) = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\}$
6	1 5	eqtri	$⊢ F = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\}$
7	4 6	ovidi	$⊢ (x \in A \land y \in B) \to (z = C \to x F y = z)$
8		eqeq2	$⊢ z = C \to (x F y = z \leftrightarrow x F y = C)$
9	7 8	mpbidi	$⊢ (x \in A \land y \in B) \to (z = C \to x F y = C)$
10	9	exlimdv	$⊢ (x \in A \land y \in B) \to (\exists z z = C \to x F y = C)$
11	2 10	syl5	$⊢ (x \in A \land y \in B) \to (C \in V \to x F y = C)$
12	11	3impia	$⊢ (x \in A \land y \in B \land C \in V) \to x F y = C$