Metamath Proof Explorer

Theorem dmcnvepres

Description: Domain of the restricted converse epsilon relation. (Contributed by Peter Mazsa, 28-Jan-2026)

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

Proof

Step Hyp Ref Expression
1 dmres 
 |-  dom ( `' _E |` A ) = ( A i^i dom `' _E )
2 dmcnvep 
 |-  dom `' _E = ( _V \ { (/) } )
3 2 ineq2i 
 |-  ( A i^i dom `' _E ) = ( A i^i ( _V \ { (/) } ) )
4 invdif 
 |-  ( A i^i ( _V \ { (/) } ) ) = ( A \ { (/) } )
5 1 3 4 3eqtri 
 |-  dom ( `' _E |` A ) = ( A \ { (/) } )