Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Alternative definitions of function values (2)
fundmafv2rnb
Metamath Proof Explorer
Description: The alternate function value at a class A is defined, i.e., in the
range of the function iff A is in the domain of the function.
(Contributed by AV , 3-Sep-2022)
Ref
Expression
Assertion
fundmafv2rnb
⊢ Fun ⁡ F → A ∈ dom ⁡ F ↔ F '''' A ∈ ran ⁡ F
Proof
Step
Hyp
Ref
Expression
1
funres
⊢ Fun ⁡ F → Fun ⁡ F ↾ A
2
dmafv2rnb
⊢ Fun ⁡ F ↾ A → A ∈ dom ⁡ F ↔ F '''' A ∈ ran ⁡ F
3
1 2
syl
⊢ Fun ⁡ F → A ∈ dom ⁡ F ↔ F '''' A ∈ ran ⁡ F