Metamath Proof Explorer

Theorem dmexd

Description: The domain of a set is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypothesis dmexd.1 φ A V
Assertion dmexd φ dom A V


Step Hyp Ref Expression
1 dmexd.1 φ A V
2 dmexg A V dom A V
3 1 2 syl φ dom A V