Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Alternative definitions of function and operation values
Alternative definition of the value of an operation
nfunsnaov
Metamath Proof Explorer
Description: If the restriction of a class to a singleton is not a function, its
operation value is the universal class. (Contributed by Alexander van der
Vekens , 26-May-2017)
Ref
Expression
Assertion
nfunsnaov
⊢ ¬ Fun ⁡ F ↾ A B → A F B = V
Proof
Step
Hyp
Ref
Expression
1
df-aov
⊢ A F B = F ''' A B
2
nfunsnafv
⊢ ¬ Fun ⁡ F ↾ A B → F ''' A B = V
3
1 2
syl5eq
⊢ ¬ Fun ⁡ F ↾ A B → A F B = V