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

Metamath Proof Explorer

Theorem ovidig

Description: The value of an operation class abstraction. Compare ovidi . The condition ( x e. R /\ y e. S ) is been removed. (Contributed by Mario Carneiro, 29-Dec-2014)

Ref Expression
Hypotheses ovidig.1 
|- E* z ph
ovidig.2 
|- F = { <. <. x , y >. , z >. | ph }
Assertion ovidig 
|- ( ph -> ( x F y ) = z )

Proof

Step Hyp Ref Expression
1 ovidig.1 
 |-  E* z ph
2 ovidig.2 
 |-  F = { <. <. x , y >. , z >. | ph }
3 df-ov 
 |-  ( x F y ) = ( F ` <. x , y >. )
4 1 funoprab 
 |-  Fun { <. <. x , y >. , z >. | ph }
5 2 funeqi 
 |-  ( Fun F <-> Fun { <. <. x , y >. , z >. | ph } )
6 4 5 mpbir 
 |-  Fun F
7 oprabidw 
 |-  ( <. <. x , y >. , z >. e. { <. <. x , y >. , z >. | ph } <-> ph )
8 7 biimpri 
 |-  ( ph -> <. <. x , y >. , z >. e. { <. <. x , y >. , z >. | ph } )
9 8 2 eleqtrrdi 
 |-  ( ph -> <. <. x , y >. , z >. e. F )
10 funopfv 
 |-  ( Fun F -> ( <. <. x , y >. , z >. e. F -> ( F ` <. x , y >. ) = z ) )
11 6 9 10 mpsyl 
 |-  ( ph -> ( F ` <. x , y >. ) = z )
12 3 11 eqtrid 
 |-  ( ph -> ( x F y ) = z )