This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 \leftrightarrow \forall x x \in dom E$
2		el	$⊢ \exists y x \in y$
3		epel	$⊢ x E y \leftrightarrow x \in y$
4	3	exbii	$⊢ \exists y x E y \leftrightarrow \exists y x \in y$
5	2 4	mpbir	$⊢ \exists y x E y$
6		vex	$⊢ x \in V$
7	6	eldm	$⊢ x \in dom E \leftrightarrow \exists y x E y$
8	5 7	mpbir	$⊢ x \in dom E$
9	1 8	mpgbir	$⊢ dom E = V$