Theorem ovssunirn

Description: The result of an operation value is always a subset of the union of the range. (Contributed by Mario Carneiro, 12-Jan-2017)

	Ref	Expression
Assertion	ovssunirn	⊢ ( 𝑋 𝐹 𝑌 ) ⊆ ∪ ran 𝐹

Proof

Step	Hyp	Ref	Expression
1		df-ov	⊢ ( 𝑋 𝐹 𝑌 ) = ( 𝐹 ‘ ⟨ 𝑋 , 𝑌 ⟩ )
2		fvssunirn	⊢ ( 𝐹 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ⊆ ∪ ran 𝐹
3	1 2	eqsstri	⊢ ( 𝑋 𝐹 𝑌 ) ⊆ ∪ ran 𝐹