Metamath Proof Explorer


Theorem dffun6

Description: Alternate definition of a function using "at most one" notation. (Contributed by NM, 9-Mar-1995) Avoid ax-10 , ax-12 . (Revised by SN, 19-Dec-2024)

Ref Expression
Assertion dffun6
|- ( Fun F <-> ( Rel F /\ A. x E* y x F y ) )

Proof

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