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

Metamath Proof Explorer

Theorem ovid

Description: The value of an operation class abstraction. (Contributed by NM, 16-May-1995) (Revised by David Abernethy, 19-Jun-2012)

Ref Expression
Hypotheses ovid.1 
|- ( ( x e. R /\ y e. S ) -> E! z ph )
ovid.2 
|- F = { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) }
Assertion ovid 
|- ( ( x e. R /\ y e. S ) -> ( ( x F y ) = z <-> ph ) )

Proof

Step Hyp Ref Expression
1 ovid.1 
 |-  ( ( x e. R /\ y e. S ) -> E! z ph )
2 ovid.2 
 |-  F = { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) }
3 df-ov 
 |-  ( x F y ) = ( F ` <. x , y >. )
4 3 eqeq1i 
 |-  ( ( x F y ) = z <-> ( F ` <. x , y >. ) = z )
5 1 fnoprab 
 |-  { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) } Fn { <. x , y >. | ( x e. R /\ y e. S ) }
6 2 fneq1i 
 |-  ( F Fn { <. x , y >. | ( x e. R /\ y e. S ) } <-> { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) } Fn { <. x , y >. | ( x e. R /\ y e. S ) } )
7 5 6 mpbir 
 |-  F Fn { <. x , y >. | ( x e. R /\ y e. S ) }
8 opabidw 
 |-  ( <. x , y >. e. { <. x , y >. | ( x e. R /\ y e. S ) } <-> ( x e. R /\ y e. S ) )
9 8 biimpri 
 |-  ( ( x e. R /\ y e. S ) -> <. x , y >. e. { <. x , y >. | ( x e. R /\ y e. S ) } )
10 fnopfvb 
 |-  ( ( F Fn { <. x , y >. | ( x e. R /\ y e. S ) } /\ <. x , y >. e. { <. x , y >. | ( x e. R /\ y e. S ) } ) -> ( ( F ` <. x , y >. ) = z <-> <. <. x , y >. , z >. e. F ) )
11 7 9 10 sylancr 
 |-  ( ( x e. R /\ y e. S ) -> ( ( F ` <. x , y >. ) = z <-> <. <. x , y >. , z >. e. F ) )
12 2 eleq2i 
 |-  ( <. <. x , y >. , z >. e. F <-> <. <. x , y >. , z >. e. { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) } )
13 oprabidw 
 |-  ( <. <. x , y >. , z >. e. { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) } <-> ( ( x e. R /\ y e. S ) /\ ph ) )
14 12 13 bitri 
 |-  ( <. <. x , y >. , z >. e. F <-> ( ( x e. R /\ y e. S ) /\ ph ) )
15 14 baib 
 |-  ( ( x e. R /\ y e. S ) -> ( <. <. x , y >. , z >. e. F <-> ph ) )
16 11 15 bitrd 
 |-  ( ( x e. R /\ y e. S ) -> ( ( F ` <. x , y >. ) = z <-> ph ) )
17 4 16 bitrid 
 |-  ( ( x e. R /\ y e. S ) -> ( ( x F y ) = z <-> ph ) )