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

Metamath Proof Explorer

Theorem ovigg

Description: The value of an operation class abstraction. Compared with ovig , the condition ( x e. R /\ y e. S ) is removed. (Contributed by FL, 24-Mar-2007) (Revised by Mario Carneiro, 19-Dec-2013)

Ref Expression
Hypotheses ovigg.1 
|- ( ( x = A /\ y = B /\ z = C ) -> ( ph <-> ps ) )
ovigg.4 
|- E* z ph
ovigg.5 
|- F = { <. <. x , y >. , z >. | ph }
Assertion ovigg 
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( ps -> ( A F B ) = C ) )

Proof

Step Hyp Ref Expression
1 ovigg.1 
 |-  ( ( x = A /\ y = B /\ z = C ) -> ( ph <-> ps ) )
2 ovigg.4 
 |-  E* z ph
3 ovigg.5 
 |-  F = { <. <. x , y >. , z >. | ph }
4 1 eloprabga 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( <. <. A , B >. , C >. e. { <. <. x , y >. , z >. | ph } <-> ps ) )
5 df-ov 
 |-  ( A F B ) = ( F ` <. A , B >. )
6 3 fveq1i 
 |-  ( F ` <. A , B >. ) = ( { <. <. x , y >. , z >. | ph } ` <. A , B >. )
7 5 6 eqtri 
 |-  ( A F B ) = ( { <. <. x , y >. , z >. | ph } ` <. A , B >. )
8 2 funoprab 
 |-  Fun { <. <. x , y >. , z >. | ph }
9 funopfv 
 |-  ( Fun { <. <. x , y >. , z >. | ph } -> ( <. <. A , B >. , C >. e. { <. <. x , y >. , z >. | ph } -> ( { <. <. x , y >. , z >. | ph } ` <. A , B >. ) = C ) )
10 8 9 ax-mp 
 |-  ( <. <. A , B >. , C >. e. { <. <. x , y >. , z >. | ph } -> ( { <. <. x , y >. , z >. | ph } ` <. A , B >. ) = C )
11 7 10 eqtrid 
 |-  ( <. <. A , B >. , C >. e. { <. <. x , y >. , z >. | ph } -> ( A F B ) = C )
12 4 11 biimtrrdi 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( ps -> ( A F B ) = C ) )