Theorem fvilbdRP

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

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

Proof

Step	Hyp	Ref	Expression
1		fvilbdRP.r	$$⊢\phi \to R\in \mathrm{V}$$
2		dfid6	$$⊢\mathrm{I}=\left(r\in \mathrm{V}⟼\bigcup _{n\in \left\{1\right\}}\left(r{\uparrow }_{r}n\right)\right)$$
3		snex	$$⊢\left\{1\right\}\in \mathrm{V}$$
4	3	a1i	$$⊢\phi \to \left\{1\right\}\in \mathrm{V}$$
5		1ex	$$⊢1\in \mathrm{V}$$
6	5	snid	$$⊢1\in \left\{1\right\}$$
7	6	a1i	$$⊢\phi \to 1\in \left\{1\right\}$$
8	2 1 4 7	fvmptiunrelexplb1d	$$⊢\phi \to R\subseteq \mathrm{I}\left(R\right)$$