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	|- dom _E = _V

Proof

Step	Hyp	Ref	Expression
1		eqv	|- ( dom _E = _V <-> A. x x e. dom _E )
2		el	|- E. y x e. y
3		epel	|- ( x _E y <-> x e. y )
4	3	exbii	|- ( E. y x _E y <-> E. y x e. y )
5	2 4	mpbir	|- E. y x _E y
6		vex	|- x e. _V
7	6	eldm	|- ( x e. dom _E <-> E. y x _E y )
8	5 7	mpbir	|- x e. dom _E
9	1 8	mpgbir	|- dom _E = _V