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 x * y x F y

Proof

Step Hyp Ref Expression
1 dffun2 Fun F Rel F x y z x F y x F z y = z
2 breq2 y = z x F y x F z
3 2 mo4 * y x F y y z x F y x F z y = z
4 3 albii x * y x F y x y z x F y x F z y = z
5 4 anbi2i Rel F x * y x F y Rel F x y z x F y x F z y = z
6 1 5 bitr4i Fun F Rel F x * y x F y