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