Metamath Proof Explorer


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