Theorem funopab

Description: A class of ordered pairs is a function when there is at most one second member for each pair. (Contributed by NM, 16-May-1995)

	Ref	Expression
Assertion	funopab	|- ( Fun { <. x , y >. | ph } <-> A. x E* y ph )

Proof

Step	Hyp	Ref	Expression
1		relopab	|- Rel { <. x , y >. | ph }
2		nfopab1	|- F/_ x { <. x , y >. | ph }
3		nfopab2	|- F/_ y { <. x , y >. | ph }
4	2 3	dffun6f	|- ( Fun { <. x , y >. | ph } <-> ( Rel { <. x , y >. | ph } /\ A. x E* y x { <. x , y >. | ph } y ) )
5	1 4	mpbiran	|- ( Fun { <. x , y >. | ph } <-> A. x E* y x { <. x , y >. | ph } y )
6		df-br	|- ( x { <. x , y >. | ph } y <-> <. x , y >. e. { <. x , y >. | ph } )
7		opabidw	|- ( <. x , y >. e. { <. x , y >. | ph } <-> ph )
8	6 7	bitri	|- ( x { <. x , y >. | ph } y <-> ph )
9	8	mobii	|- ( E* y x { <. x , y >. | ph } y <-> E* y ph )
10	9	albii	|- ( A. x E* y x { <. x , y >. | ph } y <-> A. x E* y ph )
11	5 10	bitri	|- ( Fun { <. x , y >. | ph } <-> A. x E* y ph )