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

Metamath Proof Explorer

Theorem resex

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

Ref Expression
Hypothesis resex.1 ⊢ A ∈ V
Assertion resex ⊢ A ↾ B ∈ V

Proof

Step Hyp Ref Expression
1 resex.1 ⊢ A ∈ V
2 resexg ⊢ A ∈ V → A ↾ B ∈ V
3 1 2 ax-mp ⊢ A ↾ B ∈ V