Description: Alternate definition of function, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Emmett Weisz, 14-Mar-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dffun3f.1 | ⊢ Ⅎ 𝑥 𝐴 | |
dffun3f.2 | ⊢ Ⅎ 𝑦 𝐴 | ||
dffun3f.3 | ⊢ Ⅎ 𝑧 𝐴 | ||
Assertion | dffun3f | ⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑦 = 𝑧 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dffun3f.1 | ⊢ Ⅎ 𝑥 𝐴 | |
2 | dffun3f.2 | ⊢ Ⅎ 𝑦 𝐴 | |
3 | dffun3f.3 | ⊢ Ⅎ 𝑧 𝐴 | |
4 | 1 2 | dffun6f | ⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 ) ) |
5 | nfcv | ⊢ Ⅎ 𝑧 𝑥 | |
6 | nfcv | ⊢ Ⅎ 𝑧 𝑦 | |
7 | 5 3 6 | nfbr | ⊢ Ⅎ 𝑧 𝑥 𝐴 𝑦 |
8 | 7 | mof | ⊢ ( ∃* 𝑦 𝑥 𝐴 𝑦 ↔ ∃ 𝑧 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑦 = 𝑧 ) ) |
9 | 8 | albii | ⊢ ( ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 ↔ ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑦 = 𝑧 ) ) |
10 | 9 | anbi2i | ⊢ ( ( Rel 𝐴 ∧ ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 ) ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑦 = 𝑧 ) ) ) |
11 | 4 10 | bitri | ⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ∀ 𝑥 ∃ 𝑧 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑦 = 𝑧 ) ) ) |