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 ) C_ U. ran F

Proof

Step	Hyp	Ref	Expression
1		fvrn0	|- ( F ` X ) e. ( ran F u. { (/) } )
2		elssuni	|- ( ( F ` X ) e. ( ran F u. { (/) } ) -> ( F ` X ) C_ U. ( ran F u. { (/) } ) )
3	1 2	ax-mp	|- ( F ` X ) C_ U. ( ran F u. { (/) } )
4		uniun	|- U. ( ran F u. { (/) } ) = ( U. ran F u. U. { (/) } )
5		0ex	|- (/) e. _V
6	5	unisn	|- U. { (/) } = (/)
7	6	uneq2i	|- ( U. ran F u. U. { (/) } ) = ( U. ran F u. (/) )
8		un0	|- ( U. ran F u. (/) ) = U. ran F
9	4 7 8	3eqtri	|- U. ( ran F u. { (/) } ) = U. ran F
10	3 9	sseqtri	|- ( F ` X ) C_ U. ran F