Theorem resex

Description: The restriction of a set is a set. (Contributed by Jeff Madsen, 19-Jun-2011)

	Ref	Expression
Hypothesis	resex.1	⊢ 𝐴 ∈ V
Assertion	resex	⊢ ( 𝐴 ↾ 𝐵 ) ∈ V

Proof

Step	Hyp	Ref	Expression
1		resex.1	⊢ 𝐴 ∈ V
2		resexg	⊢ ( 𝐴 ∈ V → ( 𝐴 ↾ 𝐵 ) ∈ V )
3	1 2	ax-mp	⊢ ( 𝐴 ↾ 𝐵 ) ∈ V