Theorem fviss

Description: The value of the identity function is a subset of the argument. (An artifact of our function value definition.) (Contributed by Mario Carneiro, 27-Feb-2016)

	Ref	Expression
Assertion	fviss	|- ( _I ` A ) C_ A

Proof

Step	Hyp	Ref	Expression
1		id	|- ( x e. ( _I ` A ) -> x e. ( _I ` A ) )
2		elfvex	|- ( x e. ( _I ` A ) -> A e. _V )
3		fvi	|- ( A e. _V -> ( _I ` A ) = A )
4	2 3	syl	|- ( x e. ( _I ` A ) -> ( _I ` A ) = A )
5	1 4	eleqtrd	|- ( x e. ( _I ` A ) -> x e. A )
6	5	ssriv	|- ( _I ` A ) C_ A