This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fvresval

Description: The value of a restricted function at a class is either the empty set or the value of the unrestricted function at that class. (Contributed by Scott Fenton, 4-Sep-2011)

Ref Expression
Assertion fvresval ⊢ F ↾ B ⁡ A = F ⁡ A ∨ F ↾ B ⁡ A = ∅

Proof

Step Hyp Ref Expression
1 exmid ⊢ A ∈ B ∨ ¬ A ∈ B
2 fvres ⊢ A ∈ B → F ↾ B ⁡ A = F ⁡ A
3 nfvres ⊢ ¬ A ∈ B → F ↾ B ⁡ A = ∅
4 2 3 orim12i ⊢ A ∈ B ∨ ¬ A ∈ B → F ↾ B ⁡ A = F ⁡ A ∨ F ↾ B ⁡ A = ∅
5 1 4 ax-mp ⊢ F ↾ B ⁡ A = F ⁡ A ∨ F ↾ B ⁡ A = ∅