Description: A function operation restricted to a set is a set. (Contributed by NM, 28-Jul-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | ofexg | ⊢ ( 𝐴 ∈ 𝑉 → ( ∘f 𝑅 ↾ 𝐴 ) ∈ V ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-of | ⊢ ∘f 𝑅 = ( 𝑓 ∈ V , 𝑔 ∈ V ↦ ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) ) | |
2 | 1 | mpofun | ⊢ Fun ∘f 𝑅 |
3 | resfunexg | ⊢ ( ( Fun ∘f 𝑅 ∧ 𝐴 ∈ 𝑉 ) → ( ∘f 𝑅 ↾ 𝐴 ) ∈ V ) | |
4 | 2 3 | mpan | ⊢ ( 𝐴 ∈ 𝑉 → ( ∘f 𝑅 ↾ 𝐴 ) ∈ V ) |