Metamath Proof Explorer

Theorem dffun4

Description: Alternate definition of a function. Definition 6.4(4) of TakeutiZaring p. 24. (Contributed by NM, 29-Dec-1996)

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

Proof

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