Theorem ofmresex

Description: Existence of a restriction of the function operation map. (Contributed by NM, 20-Oct-2014)

	Ref	Expression
Hypotheses	ofmresex.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	ofmresex.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
Assertion	ofmresex	⊢ ( 𝜑 → ( ∘f 𝑅 ↾ ( 𝐴 × 𝐵 ) ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		ofmresex.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		ofmresex.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3	1 2	xpexd	⊢ ( 𝜑 → ( 𝐴 × 𝐵 ) ∈ V )
4		ofexg	⊢ ( ( 𝐴 × 𝐵 ) ∈ V → ( ∘f 𝑅 ↾ ( 𝐴 × 𝐵 ) ) ∈ V )
5	3 4	syl	⊢ ( 𝜑 → ( ∘f 𝑅 ↾ ( 𝐴 × 𝐵 ) ) ∈ V )