Theorem domepOLD

Description: Obsolete proof of dmep as of 26-Dec-2023. (Contributed by Scott Fenton, 27-Oct-2010) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		equid	$$⊢x=x$$
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	1 5	2th	$$⊢x=x\leftrightarrow \exists yx\mathrm{E}y$$
7	6	abbii	$$⊢\left\{x|x=x\right\}=\left\{x|\exists yx\mathrm{E}y\right\}$$
8		df-v	$$⊢\mathrm{V}=\left\{x|x=x\right\}$$
9		df-dm	$$⊢\mathrm{dom}\mathrm{E}=\left\{x|\exists yx\mathrm{E}y\right\}$$
10	7 8 9	3eqtr4ri	$$⊢\mathrm{dom}\mathrm{E}=\mathrm{V}$$