Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Alternative definitions of function and operation values
Predicate "defined at"
fundmdfat
Next ⟩
dfatprc
Metamath Proof Explorer
Ascii
Unicode
Theorem
fundmdfat
Description:
A function is defined at any element of its domain.
(Contributed by
AV
, 2-Sep-2022)
Ref
Expression
Assertion
fundmdfat
⊢
Fun
⁡
F
∧
A
∈
dom
⁡
F
→
F
defAt
A
Proof
Step
Hyp
Ref
Expression
1
funres
⊢
Fun
⁡
F
→
Fun
⁡
F
↾
A
2
1
anim1ci
⊢
Fun
⁡
F
∧
A
∈
dom
⁡
F
→
A
∈
dom
⁡
F
∧
Fun
⁡
F
↾
A
3
df-dfat
⊢
F
defAt
A
↔
A
∈
dom
⁡
F
∧
Fun
⁡
F
↾
A
4
2
3
sylibr
⊢
Fun
⁡
F
∧
A
∈
dom
⁡
F
→
F
defAt
A