Metamath Proof Explorer

Theorem dmv

Description: The domain of the universe is the universe. (Contributed by NM, 8-Aug-2003)

Ref Expression
Assertion dmv 
|- dom _V = _V

Proof

Step Hyp Ref Expression
1 ssv 
 |-  dom _V C_ _V
2 dmi 
 |-  dom _I = _V
3 ssv 
 |-  _I C_ _V
4 dmss 
 |-  ( _I C_ _V -> dom _I C_ dom _V )
5 3 4 ax-mp 
 |-  dom _I C_ dom _V
6 2 5 eqsstrri 
 |-  _V C_ dom _V
7 1 6 eqssi 
 |-  dom _V = _V