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	⊢ dom E = V

Proof

Step	Hyp	Ref	Expression
1		equid	⊢ 𝑥 = 𝑥
2		el	⊢ ∃ 𝑦 𝑥 ∈ 𝑦
3		epel	⊢ ( 𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦 )
4	3	exbii	⊢ ( ∃ 𝑦 𝑥 E 𝑦 ↔ ∃ 𝑦 𝑥 ∈ 𝑦 )
5	2 4	mpbir	⊢ ∃ 𝑦 𝑥 E 𝑦
6	1 5	2th	⊢ ( 𝑥 = 𝑥 ↔ ∃ 𝑦 𝑥 E 𝑦 )
7	6	abbii	⊢ { 𝑥 ∣ 𝑥 = 𝑥 } = { 𝑥 ∣ ∃ 𝑦 𝑥 E 𝑦 }
8		df-v	⊢ V = { 𝑥 ∣ 𝑥 = 𝑥 }
9		df-dm	⊢ dom E = { 𝑥 ∣ ∃ 𝑦 𝑥 E 𝑦 }
10	7 8 9	3eqtr4ri	⊢ dom E = V