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	$$⊢\mathrm{dom}\mathrm{I}=\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		eqv	$$⊢\mathrm{dom}\mathrm{I}=\mathrm{V}\leftrightarrow \forall xx\in \mathrm{dom}\mathrm{I}$$
2		ax6ev	$$⊢\exists yy=x$$
3		vex	$$⊢y\in \mathrm{V}$$
4	3	ideq	$$⊢x\mathrm{I}y\leftrightarrow x=y$$
5		equcom	$$⊢x=y\leftrightarrow y=x$$
6	4 5	bitri	$$⊢x\mathrm{I}y\leftrightarrow y=x$$
7	6	exbii	$$⊢\exists yx\mathrm{I}y\leftrightarrow \exists yy=x$$
8	2 7	mpbir	$$⊢\exists yx\mathrm{I}y$$
9		vex	$$⊢x\in \mathrm{V}$$
10	9	eldm	$$⊢x\in \mathrm{dom}\mathrm{I}\leftrightarrow \exists yx\mathrm{I}y$$
11	8 10	mpbir	$$⊢x\in \mathrm{dom}\mathrm{I}$$
12	1 11	mpgbir	$$⊢\mathrm{dom}\mathrm{I}=\mathrm{V}$$