Theorem opabiotafun

Description: Define a function whose value is "the unique y such that ph ( x , y ) ". (Contributed by NM, 19-May-2015)

	Ref	Expression
Hypothesis	opabiota.1	|- F = { <. x , y >. | { y | ph } = { y } }
Assertion	opabiotafun	|- Fun F

Proof

Step	Hyp	Ref	Expression
1		opabiota.1	|- F = { <. x , y >. | { y | ph } = { y } }
2		funopab	|- ( Fun { <. x , y >. | { y | ph } = { y } } <-> A. x E* y { y | ph } = { y } )
3		mo2icl	|- ( A. z ( { y | ph } = { z } -> z = U. { y | ph } ) -> E* z { y | ph } = { z } )
4		unieq	|- ( { y | ph } = { z } -> U. { y | ph } = U. { z } )
5		vex	|- z e. _V
6	5	unisn	|- U. { z } = z
7	4 6	eqtr2di	|- ( { y | ph } = { z } -> z = U. { y | ph } )
8	3 7	mpg	|- E* z { y | ph } = { z }
9		nfv	|- F/ z { y | ph } = { y }
10		nfab1	|- F/_ y { y | ph }
11	10	nfeq1	|- F/ y { y | ph } = { z }
12		sneq	|- ( y = z -> { y } = { z } )
13	12	eqeq2d	|- ( y = z -> ( { y | ph } = { y } <-> { y | ph } = { z } ) )
14	9 11 13	cbvmow	|- ( E* y { y | ph } = { y } <-> E* z { y | ph } = { z } )
15	8 14	mpbir	|- E* y { y | ph } = { y }
16	2 15	mpgbir	|- Fun { <. x , y >. | { y | ph } = { y } }
17	1	funeqi	|- ( Fun F <-> Fun { <. x , y >. | { y | ph } = { y } } )
18	16 17	mpbir	|- Fun F