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 ↔ ∀ 𝑥 𝑥 ∈ dom I )
2		ax6ev	⊢ ∃ 𝑦 𝑦 = 𝑥
3		vex	⊢ 𝑦 ∈ V
4	3	ideq	⊢ ( 𝑥 I 𝑦 ↔ 𝑥 = 𝑦 )
5		equcom	⊢ ( 𝑥 = 𝑦 ↔ 𝑦 = 𝑥 )
6	4 5	bitri	⊢ ( 𝑥 I 𝑦 ↔ 𝑦 = 𝑥 )
7	6	exbii	⊢ ( ∃ 𝑦 𝑥 I 𝑦 ↔ ∃ 𝑦 𝑦 = 𝑥 )
8	2 7	mpbir	⊢ ∃ 𝑦 𝑥 I 𝑦
9		vex	⊢ 𝑥 ∈ V
10	9	eldm	⊢ ( 𝑥 ∈ dom I ↔ ∃ 𝑦 𝑥 I 𝑦 )
11	8 10	mpbir	⊢ 𝑥 ∈ dom I
12	1 11	mpgbir	⊢ dom I = V