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	⊢ ( 𝜑 → 𝑅 ∈ V )
Assertion	fvilbdRP	⊢ ( 𝜑 → 𝑅 ⊆ ( I ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		fvilbdRP.r	⊢ ( 𝜑 → 𝑅 ∈ V )
2		dfid6	⊢ I = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ { 1 } ( 𝑟 ↑𝑟 𝑛 ) )
3		snex	⊢ { 1 } ∈ V
4	3	a1i	⊢ ( 𝜑 → { 1 } ∈ V )
5		1ex	⊢ 1 ∈ V
6	5	snid	⊢ 1 ∈ { 1 }
7	6	a1i	⊢ ( 𝜑 → 1 ∈ { 1 } )
8	2 1 4 7	fvmptiunrelexplb1d	⊢ ( 𝜑 → 𝑅 ⊆ ( I ‘ 𝑅 ) )