This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dffun6

Description: Alternate definition of a function using "at most one" notation. (Contributed by NM, 9-Mar-1995) Avoid ax-10 , ax-12 . (Revised by SN, 19-Dec-2024)

Ref Expression
Assertion dffun6 ⊢ Fun ⁡ F ↔ Rel ⁡ F ∧ ∀ x ∃* y x F y

Proof

Step Hyp Ref Expression
1 dffun2 ⊢ Fun ⁡ F ↔ Rel ⁡ F ∧ ∀ x ∀ y ∀ z x F y ∧ x F z → y = z
2 breq2 ⊢ y = z → x F y ↔ x F z
3 2 mo4 ⊢ ∃* y x F y ↔ ∀ y ∀ z x F y ∧ x F z → y = z
4 3 albii ⊢ ∀ x ∃* y x F y ↔ ∀ x ∀ y ∀ z x F y ∧ x F z → y = z
5 4 anbi2i ⊢ Rel ⁡ F ∧ ∀ x ∃* y x F y ↔ Rel ⁡ F ∧ ∀ x ∀ y ∀ z x F y ∧ x F z → y = z
6 1 5 bitr4i ⊢ Fun ⁡ F ↔ Rel ⁡ F ∧ ∀ x ∃* y x F y