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 does not 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