Metamath Proof Explorer


Theorem dmexg

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

Ref Expression
Assertion dmexg A V dom A V

Proof

Step Hyp Ref Expression
1 uniexg A V A V
2 uniexg A V A V
3 ssun1 dom A dom A ran A
4 dmrnssfld dom A ran A A
5 3 4 sstri dom A A
6 ssexg dom A A A V dom A V
7 5 6 mpan A V dom A V
8 1 2 7 3syl A V dom A V