**Description:** The value of a function at a restriction is either null or the same as the
function itself. (Contributed by Scott Fenton, 4-Sep-2011)

Ref | Expression | ||
---|---|---|---|

Assertion | fvresval | ⊢ ( ( ( 𝐹 ↾ 𝐵 ) ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) ∨ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝐴 ) = ∅ ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | exmid | ⊢ ( 𝐴 ∈ 𝐵 ∨ ¬ 𝐴 ∈ 𝐵 ) | |

2 | fvres | ⊢ ( 𝐴 ∈ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) ) | |

3 | nfvres | ⊢ ( ¬ 𝐴 ∈ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝐴 ) = ∅ ) | |

4 | 2 3 | orim12i | ⊢ ( ( 𝐴 ∈ 𝐵 ∨ ¬ 𝐴 ∈ 𝐵 ) → ( ( ( 𝐹 ↾ 𝐵 ) ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) ∨ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝐴 ) = ∅ ) ) |

5 | 1 4 | ax-mp | ⊢ ( ( ( 𝐹 ↾ 𝐵 ) ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) ∨ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝐴 ) = ∅ ) |