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

Metamath Proof Explorer

Theorem dmresexg

Description: The domain of a restriction to a set exists. (Contributed by NM, 7-Apr-1995)

Ref Expression
Assertion dmresexg ⊢ B ∈ V → dom ⁡ A ↾ B ∈ V

Proof

Step Hyp Ref Expression
1 dmres ⊢ dom ⁡ A ↾ B = B ∩ dom ⁡ A
2 inex1g ⊢ B ∈ V → B ∩ dom ⁡ A ∈ V
3 1 2 eqeltrid ⊢ B ∈ V → dom ⁡ A ↾ B ∈ V