Metamath Proof Explorer

Theorem dffun3

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

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

Proof

Step Hyp Ref Expression
1 dffun2 
 |-  ( Fun A <-> ( Rel A /\ A. x A. y A. z ( ( x A y /\ x A z ) -> y = z ) ) )
2 breq2 
 |-  ( y = z -> ( x A y <-> x A z ) )
3 2 mo4 
 |-  ( E* y x A y <-> A. y A. z ( ( x A y /\ x A z ) -> y = z ) )
4 df-mo 
 |-  ( E* y x A y <-> E. z A. y ( x A y -> y = z ) )
5 3 4 bitr3i 
 |-  ( A. y A. z ( ( x A y /\ x A z ) -> y = z ) <-> E. z A. y ( x A y -> y = z ) )
6 5 albii 
 |-  ( A. x A. y A. z ( ( x A y /\ x A z ) -> y = z ) <-> A. x E. z A. y ( x A y -> y = z ) )
7 6 anbi2i 
 |-  ( ( Rel A /\ A. x A. y A. z ( ( x A y /\ x A z ) -> y = z ) ) <-> ( Rel A /\ A. x E. z A. y ( x A y -> y = z ) ) )
8 1 7 bitri 
 |-  ( Fun A <-> ( Rel A /\ A. x E. z A. y ( x A y -> y = z ) ) )