Metamath Proof Explorer

Theorem dffun3

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

Ref Expression
Assertion dffun3 ⊢ Fun ⁡ A ↔ Rel ⁡ A ∧ ∀ x ∃ z ∀ y x A y → 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 breq2 ⊢ y = z → x A y ↔ x A z
3 2 mo4 ⊢ ∃* y x A y ↔ ∀ y ∀ z x A y ∧ x A z → y = z
4 df-mo ⊢ ∃* y x A y ↔ ∃ z ∀ y x A y → y = z
5 3 4 bitr3i ⊢ ∀ y ∀ z x A y ∧ x A z → y = z ↔ ∃ z ∀ y x A y → y = z
6 5 albii ⊢ ∀ x ∀ y ∀ z x A y ∧ x A z → y = z ↔ ∀ x ∃ z ∀ y x A y → y = z
7 6 anbi2i ⊢ Rel ⁡ A ∧ ∀ x ∀ y ∀ z x A y ∧ x A z → y = z ↔ Rel ⁡ A ∧ ∀ x ∃ z ∀ y x A y → y = z
8 1 7 bitri ⊢ Fun ⁡ A ↔ Rel ⁡ A ∧ ∀ x ∃ z ∀ y x A y → y = z