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	⊢ ( 𝐵 ∈ ( 𝐹 ‘ 𝐴 ) → 𝐵 ∈ ∪ ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		ne0i	⊢ ( 𝐵 ∈ ( 𝐹 ‘ 𝐴 ) → ( 𝐹 ‘ 𝐴 ) ≠ ∅ )
2		fvn0fvelrn	⊢ ( ( 𝐹 ‘ 𝐴 ) ≠ ∅ → ( 𝐹 ‘ 𝐴 ) ∈ ran 𝐹 )
3		elssuni	⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ran 𝐹 → ( 𝐹 ‘ 𝐴 ) ⊆ ∪ ran 𝐹 )
4	1 2 3	3syl	⊢ ( 𝐵 ∈ ( 𝐹 ‘ 𝐴 ) → ( 𝐹 ‘ 𝐴 ) ⊆ ∪ ran 𝐹 )
5	4	sseld	⊢ ( 𝐵 ∈ ( 𝐹 ‘ 𝐴 ) → ( 𝐵 ∈ ( 𝐹 ‘ 𝐴 ) → 𝐵 ∈ ∪ ran 𝐹 ) )
6	5	pm2.43i	⊢ ( 𝐵 ∈ ( 𝐹 ‘ 𝐴 ) → 𝐵 ∈ ∪ ran 𝐹 )