This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem resexg

Description: The restriction of a set is a set. (Contributed by NM, 28-Mar-1998) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion resexg ⊢ A ∈ V → A ↾ B ∈ V

Proof

Step Hyp Ref Expression
1 resss ⊢ A ↾ B ⊆ A
2 ssexg ⊢ A ↾ B ⊆ A ∧ A ∈ V → A ↾ B ∈ V
3 1 2 mpan ⊢ A ∈ V → A ↾ B ∈ V