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 )