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

Metamath Proof Explorer

Theorem feqresmptf

Description: Express a restricted function as a mapping. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses feqresmptf.1 ⊢ Ⅎ _ x F
feqresmptf.2 ⊢ φ → F : A ⟶ B
feqresmptf.3 ⊢ φ → C ⊆ A
Assertion feqresmptf ⊢ φ → F ↾ C = x ∈ C ⟼ F ⁡ x

Proof

Step Hyp Ref Expression
1 feqresmptf.1 ⊢ Ⅎ _ x F
2 feqresmptf.2 ⊢ φ → F : A ⟶ B
3 feqresmptf.3 ⊢ φ → C ⊆ A
4 nfcv ⊢ Ⅎ _ x C
5 1 4 nfres ⊢ Ⅎ _ x F ↾ C
6 2 3 fssresd ⊢ φ → F ↾ C : C ⟶ B
7 4 5 6 feqmptdf ⊢ φ → F ↾ C = x ∈ C ⟼ F ↾ C ⁡ x
8 fvres ⊢ x ∈ C → F ↾ C ⁡ x = F ⁡ x
9 8 mpteq2ia ⊢ x ∈ C ⟼ F ↾ C ⁡ x = x ∈ C ⟼ F ⁡ x
10 7 9 eqtrdi ⊢ φ → F ↾ C = x ∈ C ⟼ F ⁡ x