Theorem dmep

Description: The domain of the membership relation is the universal class. (Contributed by Scott Fenton, 27-Oct-2010) (Proof shortened by BJ, 26-Dec-2023)

	Ref	Expression
Assertion	dmep	$$⊢\mathrm{dom}\mathrm{E}=\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		eqv	$$⊢\mathrm{dom}\mathrm{E}=\mathrm{V}\leftrightarrow \forall xx\in \mathrm{dom}\mathrm{E}$$
2		el	$$⊢\exists yx\in y$$
3		epel	$$⊢x\mathrm{E}y\leftrightarrow x\in y$$
4	3	exbii	$$⊢\exists yx\mathrm{E}y\leftrightarrow \exists yx\in y$$
5	2 4	mpbir	$$⊢\exists yx\mathrm{E}y$$
6		vex	$$⊢x\in \mathrm{V}$$
7	6	eldm	$$⊢x\in \mathrm{dom}\mathrm{E}\leftrightarrow \exists yx\mathrm{E}y$$
8	5 7	mpbir	$$⊢x\in \mathrm{dom}\mathrm{E}$$
9	1 8	mpgbir	$$⊢\mathrm{dom}\mathrm{E}=\mathrm{V}$$