Theorem fvssunirn

Description: The result of a function value is always a subset of the union of the range, even if it is invalid and thus empty. (Contributed by Stefan O'Rear, 2-Nov-2014) (Revised by Mario Carneiro, 31-Aug-2015) (Proof shortened by SN, 13-Jan-2025)

	Ref	Expression
Assertion	fvssunirn	$$⊢F\left(X\right)\subseteq \bigcup \mathrm{ran}F$$

Proof

Step	Hyp	Ref	Expression
1		elfvunirn	$$⊢x\in F\left(X\right)\to x\in \bigcup \mathrm{ran}F$$
2	1	ssriv	$$⊢F\left(X\right)\subseteq \bigcup \mathrm{ran}F$$