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	$$⊢XFY\subseteq \bigcup \mathrm{ran}F$$

Proof

Step	Hyp	Ref	Expression
1		df-ov	$$⊢XFY=F\left(⟨X,Y⟩\right)$$
2		fvssunirn	$$⊢F\left(⟨X,Y⟩\right)\subseteq \bigcup \mathrm{ran}F$$
3	1 2	eqsstri	$$⊢XFY\subseteq \bigcup \mathrm{ran}F$$