Description: Alternate definition of function. (Contributed by NM, 29-Dec-1996) (Proof shortened by SN, 19-Dec-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | dffun3 | ⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑦 = 𝑧 ) ) ) |
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 𝐴 ∧ ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑦 = 𝑧 ) ) ) |