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)

Ref Expression
Assertion fvssunirn F X ran F


Step Hyp Ref Expression
1 fvrn0 F X ran F
2 elssuni F X ran F F X ran F
3 1 2 ax-mp F X ran F
4 uniun ran F = ran F
5 0ex V
6 5 unisn =
7 6 uneq2i ran F = ran F
8 un0 ran F = ran F
9 4 7 8 3eqtri ran F = ran F
10 3 9 sseqtri F X ran F