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

Metamath Proof Explorer

Theorem dmcnvep

Description: Domain of converse epsilon relation. (Contributed by Peter Mazsa, 30-Jan-2018) (Revised by Peter Mazsa, 23-Nov-2025)

Ref Expression
Assertion dmcnvep 
|- dom `' _E = ( _V \ { (/) } )

Proof

Step Hyp Ref Expression
1 df-dm 
 |-  dom `' _E = { x | E. y x `' _E y }
2 brcnvep 
 |-  ( x e. _V -> ( x `' _E y <-> y e. x ) )
3 2 elv 
 |-  ( x `' _E y <-> y e. x )
4 3 exbii 
 |-  ( E. y x `' _E y <-> E. y y e. x )
5 4 abbii 
 |-  { x | E. y x `' _E y } = { x | E. y y e. x }
6 df-sn 
 |-  { (/) } = { x | x = (/) }
7 6 difeq2i 
 |-  ( _V \ { (/) } ) = ( _V \ { x | x = (/) } )
8 notab 
 |-  { x | -. x = (/) } = ( _V \ { x | x = (/) } )
9 neq0 
 |-  ( -. x = (/) <-> E. y y e. x )
10 9 abbii 
 |-  { x | -. x = (/) } = { x | E. y y e. x }
11 7 8 10 3eqtr2ri 
 |-  { x | E. y y e. x } = ( _V \ { (/) } )
12 1 5 11 3eqtri 
 |-  dom `' _E = ( _V \ { (/) } )