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 | dmafv2rnb | ⊢ ( Fun ( 𝐹 ↾ { 𝐴 } ) → ( 𝐴 ∈ dom 𝐹 ↔ ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iba | ⊢ ( Fun ( 𝐹 ↾ { 𝐴 } ) → ( 𝐴 ∈ dom 𝐹 ↔ ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ) ) | |
2 | df-dfat | ⊢ ( 𝐹 defAt 𝐴 ↔ ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ) | |
3 | dfatafv2rnb | ⊢ ( 𝐹 defAt 𝐴 ↔ ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 ) | |
4 | 2 3 | bitr3i | ⊢ ( ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ↔ ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 ) |
5 | 1 4 | bitrdi | ⊢ ( Fun ( 𝐹 ↾ { 𝐴 } ) → ( 𝐴 ∈ dom 𝐹 ↔ ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 ) ) |