This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )