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 ) )