Theorem resiexd

Description: The restriction of the identity relation to a set is a set. (Contributed by AV, 15-Feb-2020)

	Ref	Expression
Hypothesis	resiexd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
Assertion	resiexd	⊢ ( 𝜑 → ( I ↾ 𝐵 ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		resiexd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
2		funi	⊢ Fun I
3		resfunexg	⊢ ( ( Fun I ∧ 𝐵 ∈ 𝑉 ) → ( I ↾ 𝐵 ) ∈ V )
4	2 1 3	sylancr	⊢ ( 𝜑 → ( I ↾ 𝐵 ) ∈ V )