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

Metamath Proof Explorer

Theorem dmxrnuncnvepres

Description: Domain of the range Cartesian product with the converse epsilon relation combined with the union with the converse epsilon, restricted. (Contributed by Peter Mazsa, 28-Jan-2026)

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

Proof

Step Hyp Ref Expression
1 dmuncnvepres 
 |-  dom ( ( ( R |X. `' _E ) u. `' _E ) |` A ) = ( A i^i ( dom ( R |X. `' _E ) u. ( _V \ { (/) } ) ) )
2 dmxrncnvep 
 |-  dom ( R |X. `' _E ) = ( dom R \ { (/) } )
3 2 uneq1i 
 |-  ( dom ( R |X. `' _E ) u. ( _V \ { (/) } ) ) = ( ( dom R \ { (/) } ) u. ( _V \ { (/) } ) )
4 difundir 
 |-  ( ( dom R u. _V ) \ { (/) } ) = ( ( dom R \ { (/) } ) u. ( _V \ { (/) } ) )
5 unv 
 |-  ( dom R u. _V ) = _V
6 5 difeq1i 
 |-  ( ( dom R u. _V ) \ { (/) } ) = ( _V \ { (/) } )
7 3 4 6 3eqtr2i 
 |-  ( dom ( R |X. `' _E ) u. ( _V \ { (/) } ) ) = ( _V \ { (/) } )
8 7 ineq2i 
 |-  ( A i^i ( dom ( R |X. `' _E ) u. ( _V \ { (/) } ) ) ) = ( A i^i ( _V \ { (/) } ) )
9 invdif 
 |-  ( A i^i ( _V \ { (/) } ) ) = ( A \ { (/) } )
10 1 8 9 3eqtri 
 |-  dom ( ( ( R |X. `' _E ) u. `' _E ) |` A ) = ( A \ { (/) } )