Metamath Proof Explorer

Theorem dffun8

Description: Alternate definition of a function. One possibility for the definition of a function in Enderton p. 42. Compare dffun7 . (Contributed by NM, 4-Nov-2002) (Proof shortened by Andrew Salmon, 17-Sep-2011)

Ref Expression
Assertion dffun8 ⊢ Fun ⁡ A ↔ Rel ⁡ A ∧ ∀ x ∈ dom ⁡ A ∃! y x A y

Proof

Step Hyp Ref Expression
1 dffun7 ⊢ Fun ⁡ A ↔ Rel ⁡ A ∧ ∀ x ∈ dom ⁡ A ∃* y x A y
2 moeu ⊢ ∃* 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 pm5.5 ⊢ ∃ y x A y → ∃ y x A y → ∃! y x A y ↔ ∃! y x A y
6 4 5 sylbi ⊢ x ∈ dom ⁡ A → ∃ y x A y → ∃! y x A y ↔ ∃! y x A y
7 2 6 syl5bb ⊢ x ∈ dom ⁡ A → ∃* y x A y ↔ ∃! y x A y
8 7 ralbiia ⊢ ∀ x ∈ dom ⁡ A ∃* y x A y ↔ ∀ x ∈ dom ⁡ A ∃! y x A y
9 8 anbi2i ⊢ Rel ⁡ A ∧ ∀ x ∈ dom ⁡ A ∃* y x A y ↔ Rel ⁡ A ∧ ∀ x ∈ dom ⁡ A ∃! y x A y
10 1 9 bitri ⊢ Fun ⁡ A ↔ Rel ⁡ A ∧ ∀ x ∈ dom ⁡ A ∃! y x A y