Theorem elfvunirn

Description: A function value is a subset of the union of the range. (An artifact of our function value definition, compare elfvdm ). (Contributed by Thierry Arnoux, 13-Nov-2016) Remove functionhood antecedent. (Revised by SN, 10-Jan-2025)

	Ref	Expression
Assertion	elfvunirn	$$⊢B\in F\left(A\right)\to B\in \bigcup \mathrm{ran}F$$

Proof

Step	Hyp	Ref	Expression
1		ne0i	$$⊢B\in F\left(A\right)\to F\left(A\right)\ne \varnothing$$
2		fvn0fvelrn	$$⊢F\left(A\right)\ne \varnothing \to F\left(A\right)\in \mathrm{ran}F$$
3		elssuni	$$⊢F\left(A\right)\in \mathrm{ran}F\to F\left(A\right)\subseteq \bigcup \mathrm{ran}F$$
4	1 2 3	3syl	$$⊢B\in F\left(A\right)\to F\left(A\right)\subseteq \bigcup \mathrm{ran}F$$
5	4	sseld	$$⊢B\in F\left(A\right)\to \left(B\in F\left(A\right)\to B\in \bigcup \mathrm{ran}F\right)$$
6	5	pm2.43i	$$⊢B\in F\left(A\right)\to B\in \bigcup \mathrm{ran}F$$