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