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 \ { (/) } )