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		unisnv	|- U. { z } = z
6	4 5	eqtr2di	|- ( { y | ph } = { z } -> z = U. { y | ph } )
7	3 6	mpg	|- E* z { y | ph } = { z }
8		nfv	|- F/ z { y | ph } = { y }
9		nfab1	|- F/_ y { y | ph }
10	9	nfeq1	|- F/ y { y | ph } = { z }
11		sneq	|- ( y = z -> { y } = { z } )
12	11	eqeq2d	|- ( y = z -> ( { y | ph } = { y } <-> { y | ph } = { z } ) )
13	8 10 12	cbvmow	|- ( E* y { y | ph } = { y } <-> E* z { y | ph } = { z } )
14	7 13	mpbir	|- E* y { y | ph } = { y }
15	2 14	mpgbir	|- Fun { <. x , y >. | { y | ph } = { y } }
16	1	funeqi	|- ( Fun F <-> Fun { <. x , y >. | { y | ph } = { y } } )
17	15 16	mpbir	|- Fun F