Theorem fvilbd

Description: A set is a subset of its image under the identity relation. (Contributed by RP, 22-Jul-2020)

	Ref	Expression
Hypothesis	fvilbd.r	$$⊢\phi \to R\in \mathrm{V}$$
Assertion	fvilbd	$$⊢\phi \to R\subseteq \mathrm{I}\left(R\right)$$

Proof

Step	Hyp	Ref	Expression
1		fvilbd.r	$$⊢\phi \to R\in \mathrm{V}$$
2		ssid	$$⊢R\subseteq R$$
3		fvi	$$⊢R\in \mathrm{V}\to \mathrm{I}\left(R\right)=R$$
4	1 3	syl	$$⊢\phi \to \mathrm{I}\left(R\right)=R$$
5	2 4	sseqtrrid	$$⊢\phi \to R\subseteq \mathrm{I}\left(R\right)$$