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	$$⊢\mathrm{I}\left(A\right)\subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢x\in \mathrm{I}\left(A\right)\to x\in \mathrm{I}\left(A\right)$$
2		elfvex	$$⊢x\in \mathrm{I}\left(A\right)\to A\in \mathrm{V}$$
3		fvi	$$⊢A\in \mathrm{V}\to \mathrm{I}\left(A\right)=A$$
4	2 3	syl	$$⊢x\in \mathrm{I}\left(A\right)\to \mathrm{I}\left(A\right)=A$$
5	1 4	eleqtrd	$$⊢x\in \mathrm{I}\left(A\right)\to x\in A$$
6	5	ssriv	$$⊢\mathrm{I}\left(A\right)\subseteq A$$