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	syl5bb	|- ( ( x e. R /\ y e. S ) -> ( ( x F y ) = z <-> ph ) )