Metamath Proof Explorer


Theorem dffun3

Description: Alternate definition of function. (Contributed by NM, 29-Dec-1996) (Proof shortened by SN, 19-Dec-2024)

Ref Expression
Assertion dffun3 Fun A Rel A x z y x A y y = z

Proof

Step Hyp Ref Expression
1 dffun6 Fun A Rel A x * y x A y
2 df-mo * y x A y z y x A y y = z
3 2 albii x * y x A y x z y x A y y = z
4 3 anbi2i Rel A x * y x A y Rel A x z y x A y y = z
5 1 4 bitri Fun A Rel A x z y x A y y = z