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 e. _V
Assertion dmex 
|- dom A e. _V

Proof

Step Hyp Ref Expression
1 dmex.1 
 |-  A e. _V
2 dmexg 
 |-  ( A e. _V -> dom A e. _V )
3 1 2 ax-mp 
 |-  dom A e. _V