Metamath Proof Explorer

Theorem dffun5

Description: Alternate definition of function. (Contributed by NM, 29-Dec-1996)

Ref Expression
Assertion dffun5 ⊢ Fun ⁡ A ↔ Rel ⁡ A ∧ ∀ x ∃ z ∀ y x y ∈ A → y = z

Proof

Step Hyp Ref Expression
1 dffun3 ⊢ Fun ⁡ A ↔ Rel ⁡ A ∧ ∀ x ∃ z ∀ y x A y → y = z
2 df-br ⊢ x A y ↔ x y ∈ A
3 2 imbi1i ⊢ x A y → y = z ↔ x y ∈ A → y = z
4 3 albii ⊢ ∀ y x A y → y = z ↔ ∀ y x y ∈ A → y = z
5 4 exbii ⊢ ∃ z ∀ y x A y → y = z ↔ ∃ z ∀ y x y ∈ A → y = z
6 5 albii ⊢ ∀ x ∃ z ∀ y x A y → y = z ↔ ∀ x ∃ z ∀ y x y ∈ A → y = z
7 6 anbi2i ⊢ Rel ⁡ A ∧ ∀ x ∃ z ∀ y x A y → y = z ↔ Rel ⁡ A ∧ ∀ x ∃ z ∀ y x y ∈ A → y = z
8 1 7 bitri ⊢ Fun ⁡ A ↔ Rel ⁡ A ∧ ∀ x ∃ z ∀ y x y ∈ A → y = z