This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ A , y ∈ B ⟼ C
Assertion ovmpt4g ⊢ x ∈ A ∧ y ∈ B ∧ C ∈ V → x F y = C

Proof

Step Hyp Ref Expression
1 ovmpt4g.3 ⊢ F = x ∈ A , y ∈ B ⟼ C
2 elisset ⊢ C ∈ V → ∃ z z = C
3 moeq ⊢ ∃* z z = C
4 3 a1i ⊢ x ∈ A ∧ y ∈ B → ∃* z z = C
5 df-mpo ⊢ x ∈ A , y ∈ B ⟼ C = x y z | x ∈ A ∧ y ∈ B ∧ z = C
6 1 5 eqtri ⊢ F = x y z | x ∈ A ∧ y ∈ B ∧ z = C
7 4 6 ovidi ⊢ x ∈ A ∧ y ∈ B → z = C → x F y = z
8 eqeq2 ⊢ z = C → x F y = z ↔ x F y = C
9 7 8 mpbidi ⊢ x ∈ A ∧ y ∈ B → z = C → x F y = C
10 9 exlimdv ⊢ x ∈ A ∧ y ∈ B → ∃ z z = C → x F y = C
11 2 10 syl5 ⊢ x ∈ A ∧ y ∈ B → C ∈ V → x F y = C
12 11 3impia ⊢ x ∈ A ∧ y ∈ B ∧ C ∈ V → x F y = C