Theorem ovidi

Description: The value of an operation class abstraction (weak version). (Contributed by Mario Carneiro, 29-Dec-2014)

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

Proof

Step	Hyp	Ref	Expression
1		ovidi.2	|- ( ( x e. R /\ y e. S ) -> E* z ph )
2		ovidi.3	|- F = { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) }
3		moanimv	|- ( E* z ( ( x e. R /\ y e. S ) /\ ph ) <-> ( ( x e. R /\ y e. S ) -> E* z ph ) )
4	1 3	mpbir	|- E* z ( ( x e. R /\ y e. S ) /\ ph )
5	4 2	ovidig	|- ( ( ( x e. R /\ y e. S ) /\ ph ) -> ( x F y ) = z )
6	5	ex	|- ( ( x e. R /\ y e. S ) -> ( ph -> ( x F y ) = z ) )