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 𝐹