Metamath Proof Explorer

Theorem dmi

Description: The domain of the identity relation is the universe. (Contributed by NM, 30-Apr-1998) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion dmi 
|- dom _I = _V

Proof

Step Hyp Ref Expression
1 eqv 
 |-  ( dom _I = _V <-> A. x x e. dom _I )
2 ax6ev 
 |-  E. y y = x
3 vex 
 |-  y e. _V
4 3 ideq 
 |-  ( x _I y <-> x = y )
5 equcom 
 |-  ( x = y <-> y = x )
6 4 5 bitri 
 |-  ( x _I y <-> y = x )
7 6 exbii 
 |-  ( E. y x _I y <-> E. y y = x )
8 2 7 mpbir 
 |-  E. y x _I y
9 vex 
 |-  x e. _V
10 9 eldm 
 |-  ( x e. dom _I <-> E. y x _I y )
11 8 10 mpbir 
 |-  x e. dom _I
12 1 11 mpgbir 
 |-  dom _I = _V