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

Metamath Proof Explorer

Theorem dffun4

Description: Alternate definition of a function. Definition 6.4(4) of TakeutiZaring p. 24. (Contributed by NM, 29-Dec-1996)

Ref Expression
Assertion dffun4 
|- ( Fun A <-> ( Rel A /\ A. x A. y A. z ( ( <. x , y >. e. A /\ <. x , z >. e. A ) -> 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 df-br 
 |-  ( x A y <-> <. x , y >. e. A )
3 df-br 
 |-  ( x A z <-> <. x , z >. e. A )
4 2 3 anbi12i 
 |-  ( ( x A y /\ x A z ) <-> ( <. x , y >. e. A /\ <. x , z >. e. A ) )
5 4 imbi1i 
 |-  ( ( ( x A y /\ x A z ) -> y = z ) <-> ( ( <. x , y >. e. A /\ <. x , z >. e. A ) -> y = z ) )
6 5 albii 
 |-  ( A. z ( ( x A y /\ x A z ) -> y = z ) <-> A. z ( ( <. x , y >. e. A /\ <. x , z >. e. A ) -> y = z ) )
7 6 2albii 
 |-  ( A. x A. y A. z ( ( x A y /\ x A z ) -> y = z ) <-> A. x A. y A. z ( ( <. x , y >. e. A /\ <. x , z >. e. A ) -> y = z ) )
8 7 anbi2i 
 |-  ( ( Rel A /\ A. x A. y A. z ( ( x A y /\ x A z ) -> y = z ) ) <-> ( Rel A /\ A. x A. y A. z ( ( <. x , y >. e. A /\ <. x , z >. e. A ) -> y = z ) ) )
9 1 8 bitri 
 |-  ( Fun A <-> ( Rel A /\ A. x A. y A. z ( ( <. x , y >. e. A /\ <. x , z >. e. A ) -> y = z ) ) )