Metamath Proof Explorer


Theorem dffun7

Description: Alternate definition of a function. One possibility for the definition of a function in Enderton p. 42. (Enderton's definition is ambiguous because "there is only one" could mean either "there is at most one" or "there is exactly one." However, dffun8 shows that it doesn't matter which meaning we pick.) (Contributed by NM, 4-Nov-2002)

Ref Expression
Assertion dffun7 Fun A Rel A x dom A * y x A y

Proof

Step Hyp Ref Expression
1 dffun6 Fun A Rel A x * y x A y
2 moabs * y x A y y x A y * y x A y
3 vex x V
4 3 eldm x dom A y x A y
5 4 imbi1i x dom A * y x A y y x A y * y x A y
6 2 5 bitr4i * y x A y x dom A * y x A y
7 6 albii x * y x A y x x dom A * y x A y
8 df-ral x dom A * y x A y x x dom A * y x A y
9 7 8 bitr4i x * y x A y x dom A * y x A y
10 9 anbi2i Rel A x * y x A y Rel A x dom A * y x A y
11 1 10 bitri Fun A Rel A x dom A * y x A y