Metamath Proof Explorer

Theorem dffun2

Description: Alternate definition of a function. (Contributed by NM, 29-Dec-1996) Avoid ax-10 , ax-12 . (Revised by SN, 19-Dec-2024) Avoid ax-11 . (Revised by BTernaryTau, 29-Dec-2024)

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 cotrg 
 |-  ( ( A o. `' A ) C_ _I <-> A. y A. x A. z ( ( y `' A x /\ x A z ) -> y _I z ) )
3 breq1 
 |-  ( y = w -> ( y `' A x <-> w `' A x ) )
4 3 anbi1d 
 |-  ( y = w -> ( ( y `' A x /\ x A z ) <-> ( w `' A x /\ x A z ) ) )
5 breq1 
 |-  ( y = w -> ( y _I z <-> w _I z ) )
6 4 5 imbi12d 
 |-  ( y = w -> ( ( ( y `' A x /\ x A z ) -> y _I z ) <-> ( ( w `' A x /\ x A z ) -> w _I z ) ) )
7 6 albidv 
 |-  ( y = w -> ( A. z ( ( y `' A x /\ x A z ) -> y _I z ) <-> A. z ( ( w `' A x /\ x A z ) -> w _I z ) ) )
8 breq2 
 |-  ( x = w -> ( y `' A x <-> y `' A w ) )
9 breq1 
 |-  ( x = w -> ( x A z <-> w A z ) )
10 8 9 anbi12d 
 |-  ( x = w -> ( ( y `' A x /\ x A z ) <-> ( y `' A w /\ w A z ) ) )
11 10 imbi1d 
 |-  ( x = w -> ( ( ( y `' A x /\ x A z ) -> y _I z ) <-> ( ( y `' A w /\ w A z ) -> y _I z ) ) )
12 11 albidv 
 |-  ( x = w -> ( A. z ( ( y `' A x /\ x A z ) -> y _I z ) <-> A. z ( ( y `' A w /\ w A z ) -> y _I z ) ) )
13 7 12 alcomw 
 |-  ( A. y A. x A. z ( ( y `' A x /\ x A z ) -> y _I z ) <-> A. x A. y A. z ( ( y `' A x /\ x A z ) -> y _I z ) )
14 vex 
 |-  y e. _V
15 vex 
 |-  x e. _V
16 14 15 brcnv 
 |-  ( y `' A x <-> x A y )
17 16 anbi1i 
 |-  ( ( y `' A x /\ x A z ) <-> ( x A y /\ x A z ) )
18 vex 
 |-  z e. _V
19 18 ideq 
 |-  ( y _I z <-> y = z )
20 17 19 imbi12i 
 |-  ( ( ( y `' A x /\ x A z ) -> y _I z ) <-> ( ( x A y /\ x A z ) -> y = z ) )
21 20 3albii 
 |-  ( A. x A. y A. z ( ( y `' A x /\ x A z ) -> y _I z ) <-> A. x A. y A. z ( ( x A y /\ x A z ) -> y = z ) )
22 13 21 bitri 
 |-  ( A. y A. x A. z ( ( y `' A x /\ x A z ) -> y _I z ) <-> A. x A. y A. z ( ( x A y /\ x A z ) -> y = z ) )
23 2 22 bitri 
 |-  ( ( A o. `' A ) C_ _I <-> A. x A. y A. z ( ( x A y /\ x A z ) -> y = z ) )
24 23 anbi2i 
 |-  ( ( Rel A /\ ( A o. `' A ) C_ _I ) <-> ( Rel A /\ A. x A. y A. z ( ( x A y /\ x A z ) -> y = z ) ) )
25 1 24 bitri 
 |-  ( Fun A <-> ( Rel A /\ A. x A. y A. z ( ( x A y /\ x A z ) -> y = z ) ) )