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

Metamath Proof Explorer

Theorem ofexg

Description: A function operation restricted to a set is a set. (Contributed by NM, 28-Jul-2014)

Ref Expression
Assertion ofexg ⊢ A ∈ V → ∘ f ⁡ R ↾ A ∈ V

Proof

Step Hyp Ref Expression
1 df-of ⊢ ∘ f ⁡ R = f ∈ V , g ∈ V ⟼ x ∈ dom ⁡ f ∩ dom ⁡ g ⟼ f ⁡ x R g ⁡ x
2 1 mpofun ⊢ Fun ⁡ ∘ f ⁡ R
3 resfunexg ⊢ Fun ⁡ ∘ f ⁡ R ∧ A ∈ V → ∘ f ⁡ R ↾ A ∈ V
4 2 3 mpan ⊢ A ∈ V → ∘ f ⁡ R ↾ A ∈ V