Metamath Proof Explorer

Theorem dffun2

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

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

Proof

Step Hyp Ref Expression
1 df-fun 
 |-  ( Fun A <-> ( Rel A /\ ( A o. `' A ) C_ _I ) )
2 df-id 
 |-  _I = { <. y , z >. | y = z }
3 2 sseq2i 
 |-  ( ( A o. `' A ) C_ _I <-> ( A o. `' A ) C_ { <. y , z >. | y = z } )
4 df-co 
 |-  ( A o. `' A ) = { <. y , z >. | E. x ( y `' A x /\ x A z ) }
5 4 sseq1i 
 |-  ( ( A o. `' A ) C_ { <. y , z >. | y = z } <-> { <. y , z >. | E. x ( y `' A x /\ x A z ) } C_ { <. y , z >. | y = z } )
6 ssopab2bw 
 |-  ( { <. y , z >. | E. x ( y `' A x /\ x A z ) } C_ { <. y , z >. | y = z } <-> A. y A. z ( E. x ( y `' A x /\ x A z ) -> y = z ) )
7 3 5 6 3bitri 
 |-  ( ( A o. `' A ) C_ _I <-> A. y A. z ( E. x ( y `' A x /\ x A z ) -> y = z ) )
8 vex 
 |-  y e. _V
9 vex 
 |-  x e. _V
10 8 9 brcnv 
 |-  ( y `' A x <-> x A y )
11 10 anbi1i 
 |-  ( ( y `' A x /\ x A z ) <-> ( x A y /\ x A z ) )
12 11 exbii 
 |-  ( E. x ( y `' A x /\ x A z ) <-> E. x ( x A y /\ x A z ) )
13 12 imbi1i 
 |-  ( ( E. x ( y `' A x /\ x A z ) -> y = z ) <-> ( E. x ( x A y /\ x A z ) -> y = z ) )
14 19.23v 
 |-  ( A. x ( ( x A y /\ x A z ) -> y = z ) <-> ( E. x ( x A y /\ x A z ) -> y = z ) )
15 13 14 bitr4i 
 |-  ( ( E. x ( y `' A x /\ x A z ) -> y = z ) <-> A. x ( ( x A y /\ x A z ) -> y = z ) )
16 15 albii 
 |-  ( A. z ( E. x ( y `' A x /\ x A z ) -> y = z ) <-> A. z A. x ( ( x A y /\ x A z ) -> y = z ) )
17 alcom 
 |-  ( A. z A. x ( ( x A y /\ x A z ) -> y = z ) <-> A. x A. z ( ( x A y /\ x A z ) -> y = z ) )
18 16 17 bitri 
 |-  ( A. z ( E. x ( y `' A x /\ x A z ) -> y = z ) <-> A. x A. z ( ( x A y /\ x A z ) -> y = z ) )
19 18 albii 
 |-  ( A. y A. z ( E. x ( y `' A x /\ x A z ) -> y = z ) <-> A. y A. x A. z ( ( x A y /\ x A z ) -> y = z ) )
20 alcom 
 |-  ( A. y A. x A. z ( ( x A y /\ x A z ) -> y = z ) <-> A. x A. y A. z ( ( x A y /\ x A z ) -> y = z ) )
21 7 19 20 3bitri 
 |-  ( ( A o. `' A ) C_ _I <-> A. x A. y A. z ( ( x A y /\ x A z ) -> y = z ) )
22 21 anbi2i 
 |-  ( ( Rel A /\ ( A o. `' A ) C_ _I ) <-> ( Rel A /\ A. x A. y A. z ( ( x A y /\ x A z ) -> y = z ) ) )
23 1 22 bitri 
 |-  ( Fun A <-> ( Rel A /\ A. x A. y A. z ( ( x A y /\ x A z ) -> y = z ) ) )