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 ↔ ∀ 𝑥 𝑥 ∈ dom E )
2		el	⊢ ∃ 𝑦 𝑥 ∈ 𝑦
3		epel	⊢ ( 𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦 )
4	3	exbii	⊢ ( ∃ 𝑦 𝑥 E 𝑦 ↔ ∃ 𝑦 𝑥 ∈ 𝑦 )
5	2 4	mpbir	⊢ ∃ 𝑦 𝑥 E 𝑦
6		vex	⊢ 𝑥 ∈ V
7	6	eldm	⊢ ( 𝑥 ∈ dom E ↔ ∃ 𝑦 𝑥 E 𝑦 )
8	5 7	mpbir	⊢ 𝑥 ∈ dom E
9	1 8	mpgbir	⊢ dom E = V