This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ ( 𝐹 ‘ 𝑋 ) ⊆ ∪ ran 𝐹

Proof

Step	Hyp	Ref	Expression
1		elfvunirn	⊢ ( 𝑥 ∈ ( 𝐹 ‘ 𝑋 ) → 𝑥 ∈ ∪ ran 𝐹 )
2	1	ssriv	⊢ ( 𝐹 ‘ 𝑋 ) ⊆ ∪ ran 𝐹