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

Proof

Step	Hyp	Ref	Expression
1		fvilbd.r	⊢ ( 𝜑 → 𝑅 ∈ V )
2		ssid	⊢ 𝑅 ⊆ 𝑅
3		fvi	⊢ ( 𝑅 ∈ V → ( I ‘ 𝑅 ) = 𝑅 )
4	1 3	syl	⊢ ( 𝜑 → ( I ‘ 𝑅 ) = 𝑅 )
5	2 4	sseqtrrid	⊢ ( 𝜑 → 𝑅 ⊆ ( I ‘ 𝑅 ) )