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

Metamath Proof Explorer

Theorem dmex

Description: The domain of a set is a set. Corollary 6.8(2) of TakeutiZaring p. 26. (Contributed by NM, 7-Jul-2008)

Ref Expression
Hypothesis dmex.1 ⊢ A ∈ V
Assertion dmex ⊢ dom ⁡ A ∈ V

Proof

Step Hyp Ref Expression
1 dmex.1 ⊢ A ∈ V
2 dmexg ⊢ A ∈ V → dom ⁡ A ∈ V
3 1 2 ax-mp ⊢ dom ⁡ A ∈ V