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 𝐹 ↔ ( Rel 𝐹 ∧ ∀ 𝑥 ∃* 𝑦 𝑥 𝐹 𝑦 ) )

Proof

Step Hyp Ref Expression
1 dffun2 ( Fun 𝐹 ↔ ( Rel 𝐹 ∧ ∀ 𝑥𝑦𝑧 ( ( 𝑥 𝐹 𝑦𝑥 𝐹 𝑧 ) → 𝑦 = 𝑧 ) ) )
2 breq2 ( 𝑦 = 𝑧 → ( 𝑥 𝐹 𝑦𝑥 𝐹 𝑧 ) )
3 2 mo4 ( ∃* 𝑦 𝑥 𝐹 𝑦 ↔ ∀ 𝑦𝑧 ( ( 𝑥 𝐹 𝑦𝑥 𝐹 𝑧 ) → 𝑦 = 𝑧 ) )
4 3 albii ( ∀ 𝑥 ∃* 𝑦 𝑥 𝐹 𝑦 ↔ ∀ 𝑥𝑦𝑧 ( ( 𝑥 𝐹 𝑦𝑥 𝐹 𝑧 ) → 𝑦 = 𝑧 ) )
5 4 anbi2i ( ( Rel 𝐹 ∧ ∀ 𝑥 ∃* 𝑦 𝑥 𝐹 𝑦 ) ↔ ( Rel 𝐹 ∧ ∀ 𝑥𝑦𝑧 ( ( 𝑥 𝐹 𝑦𝑥 𝐹 𝑧 ) → 𝑦 = 𝑧 ) ) )
6 1 5 bitr4i ( Fun 𝐹 ↔ ( Rel 𝐹 ∧ ∀ 𝑥 ∃* 𝑦 𝑥 𝐹 𝑦 ) )