Description: A function is defined at any element of its domain. (Contributed by AV, 2-Sep-2022)
Ref | Expression | ||
---|---|---|---|
Assertion | fundmdfat | ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → 𝐹 defAt 𝐴 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | funres | ⊢ ( Fun 𝐹 → Fun ( 𝐹 ↾ { 𝐴 } ) ) | |
2 | 1 | anim1ci | ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ) |
3 | df-dfat | ⊢ ( 𝐹 defAt 𝐴 ↔ ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ) | |
4 | 2 3 | sylibr | ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → 𝐹 defAt 𝐴 ) |