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 ( 𝐴𝑉 → ( ∘f 𝑅𝐴 ) ∈ V )

Proof

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 )