Metamath Proof Explorer


Theorem fvssunirnOLD

Description: Obsolete version of fvssunirn as of 13-Jan-2025. (Contributed by Stefan O'Rear, 2-Nov-2014) (Revised by Mario Carneiro, 31-Aug-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion fvssunirnOLD F X ran F

Proof

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