Metamath Proof Explorer

Theorem dffun2OLD

Description: Obsolete version of dffun2 as of 29-Dec-2024. (Contributed by NM, 29-Dec-1996) Avoid ax-10 , ax-12 . (Revised by SN, 19-Dec-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion dffun2OLD 
|- ( 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 alcom 
 |-  ( 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 ) )
4 vex 
 |-  y e. _V
5 vex 
 |-  x e. _V
6 4 5 brcnv 
 |-  ( y `' A x <-> x A y )
7 6 anbi1i 
 |-  ( ( y `' A x /\ x A z ) <-> ( x A y /\ x A z ) )
8 vex 
 |-  z e. _V
9 8 ideq 
 |-  ( y _I z <-> y = z )
10 7 9 imbi12i 
 |-  ( ( ( y `' A x /\ x A z ) -> y _I z ) <-> ( ( x A y /\ x A z ) -> y = z ) )
11 10 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 ) )
12 3 11 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 ) )
13 2 12 bitri 
 |-  ( ( A o. `' A ) C_ _I <-> A. x A. y A. z ( ( x A y /\ x A z ) -> y = z ) )
14 13 anbi2i 
 |-  ( ( Rel A /\ ( A o. `' A ) C_ _I ) <-> ( Rel A /\ A. x A. y A. z ( ( x A y /\ x A z ) -> y = z ) ) )
15 1 14 bitri 
 |-  ( Fun A <-> ( Rel A /\ A. x A. y A. z ( ( x A y /\ x A z ) -> y = z ) ) )