This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ↔ ∀ x x ∈ dom ⁡ I
2 ax6ev ⊢ ∃ y y = x
3 vex ⊢ y ∈ 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 ⊢ ∃ y x I y ↔ ∃ y y = x
8 2 7 mpbir ⊢ ∃ y x I y
9 vex ⊢ x ∈ V
10 9 eldm ⊢ x ∈ dom ⁡ I ↔ ∃ y x I y
11 8 10 mpbir ⊢ x ∈ dom ⁡ I
12 1 11 mpgbir ⊢ dom ⁡ I = V