Metamath Proof Explorer

Theorem dmxrncnvep

Description: Domain of the range product with converse epsilon relation. (Contributed by Peter Mazsa, 23-Nov-2025)

Ref Expression
Assertion dmxrncnvep 
|- dom ( R |X. `' _E ) = ( dom R \ { (/) } )

Proof

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