Metamath Proof Explorer

Theorem dffun5

Description: Alternate definition of function. (Contributed by NM, 29-Dec-1996)

Ref Expression
Assertion dffun5 
|- ( Fun A <-> ( Rel A /\ A. x E. z A. y ( <. x , y >. e. A -> y = z ) ) )

Proof

Step Hyp Ref Expression
1 dffun3 
 |-  ( Fun A <-> ( Rel A /\ A. x E. z A. y ( x A y -> y = z ) ) )
2 df-br 
 |-  ( x A y <-> <. x , y >. e. A )
3 2 imbi1i 
 |-  ( ( x A y -> y = z ) <-> ( <. x , y >. e. A -> y = z ) )
4 3 albii 
 |-  ( A. y ( x A y -> y = z ) <-> A. y ( <. x , y >. e. A -> y = z ) )
5 4 exbii 
 |-  ( E. z A. y ( x A y -> y = z ) <-> E. z A. y ( <. x , y >. e. A -> y = z ) )
6 5 albii 
 |-  ( A. x E. z A. y ( x A y -> y = z ) <-> A. x E. z A. y ( <. x , y >. e. A -> y = z ) )
7 6 anbi2i 
 |-  ( ( Rel A /\ A. x E. z A. y ( x A y -> y = z ) ) <-> ( Rel A /\ A. x E. z A. y ( <. x , y >. e. A -> y = z ) ) )
8 1 7 bitri 
 |-  ( Fun A <-> ( Rel A /\ A. x E. z A. y ( <. x , y >. e. A -> y = z ) ) )