Theorem dffun3

Description: Alternate definition of function. (Contributed by NM, 29-Dec-1996) (Proof shortened by SN, 19-Dec-2024)

	Ref	Expression
Assertion	dffun3	⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑦 = 𝑧 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dffun6	⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 ) )
2		dfmo	⊢ ( ∃* 𝑦 𝑥 𝐴 𝑦 ↔ ∃ 𝑧 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑦 = 𝑧 ) )
3	2	albii	⊢ ( ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 ↔ ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑦 = 𝑧 ) )
4	3	anbi2i	⊢ ( ( Rel 𝐴 ∧ ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 ) ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑦 = 𝑧 ) ) )
5	1 4	bitri	⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑦 = 𝑧 ) ) )