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 ‘ 𝐴 ) ⊆ 𝐴

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝑥 ∈ ( I ‘ 𝐴 ) → 𝑥 ∈ ( I ‘ 𝐴 ) )
2		elfvex	⊢ ( 𝑥 ∈ ( I ‘ 𝐴 ) → 𝐴 ∈ V )
3		fvi	⊢ ( 𝐴 ∈ V → ( I ‘ 𝐴 ) = 𝐴 )
4	2 3	syl	⊢ ( 𝑥 ∈ ( I ‘ 𝐴 ) → ( I ‘ 𝐴 ) = 𝐴 )
5	1 4	eleqtrd	⊢ ( 𝑥 ∈ ( I ‘ 𝐴 ) → 𝑥 ∈ 𝐴 )
6	5	ssriv	⊢ ( I ‘ 𝐴 ) ⊆ 𝐴