Metamath Proof Explorer


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 df-mo ( ∃* 𝑦 𝑥 𝐴 𝑦 ↔ ∃ 𝑧𝑦 ( 𝑥 𝐴 𝑦𝑦 = 𝑧 ) )
3 2 albii ( ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 ↔ ∀ 𝑥𝑧𝑦 ( 𝑥 𝐴 𝑦𝑦 = 𝑧 ) )
4 3 anbi2i ( ( Rel 𝐴 ∧ ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 ) ↔ ( Rel 𝐴 ∧ ∀ 𝑥𝑧𝑦 ( 𝑥 𝐴 𝑦𝑦 = 𝑧 ) ) )
5 1 4 bitri ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥𝑧𝑦 ( 𝑥 𝐴 𝑦𝑦 = 𝑧 ) ) )