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 e. A , y e. B |-> C )
Assertion ovmpt4g 
|- ( ( x e. A /\ y e. B /\ C e. V ) -> ( x F y ) = C )

Proof

Step Hyp Ref Expression
1 ovmpt4g.3 
 |-  F = ( x e. A , y e. B |-> C )
2 elisset 
 |-  ( C e. V -> E. z z = C )
3 moeq 
 |-  E* z z = C
4 3 a1i 
 |-  ( ( x e. A /\ y e. B ) -> E* z z = C )
5 df-mpo 
 |-  ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
6 1 5 eqtri 
 |-  F = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
7 4 6 ovidi 
 |-  ( ( x e. A /\ y e. B ) -> ( z = C -> ( x F y ) = z ) )
8 eqeq2 
 |-  ( z = C -> ( ( x F y ) = z <-> ( x F y ) = C ) )
9 7 8 mpbidi 
 |-  ( ( x e. A /\ y e. B ) -> ( z = C -> ( x F y ) = C ) )
10 9 exlimdv 
 |-  ( ( x e. A /\ y e. B ) -> ( E. z z = C -> ( x F y ) = C ) )
11 2 10 syl5 
 |-  ( ( x e. A /\ y e. B ) -> ( C e. V -> ( x F y ) = C ) )
12 11 3impia 
 |-  ( ( x e. A /\ y e. B /\ C e. V ) -> ( x F y ) = C )