Metamath Proof Explorer

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 
 |-  x = x
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 1 5 2th 
 |-  ( x = x <-> E. y x _E y )
7 6 abbii 
 |-  { x | x = x } = { x | E. y x _E y }
8 df-v 
 |-  _V = { x | x = x }
9 df-dm 
 |-  dom _E = { x | E. y x _E y }
10 7 8 9 3eqtr4ri 
 |-  dom _E = _V