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

Metamath Proof Explorer

Theorem rnxrncnvepres

Description: Range of a range Cartesian product with a restriction of the converse epsilon relation. (Contributed by Peter Mazsa, 6-Dec-2021)

Ref Expression
Assertion rnxrncnvepres 
|- ran ( R |X. ( `' _E |` A ) ) = { <. x , y >. | E. u e. A ( y e. u /\ u R x ) }

Proof

Step Hyp Ref Expression
1 rnxrnres 
 |-  ran ( R |X. ( `' _E |` A ) ) = { <. x , y >. | E. u e. A ( u R x /\ u `' _E y ) }
2 brcnvep 
 |-  ( u e. _V -> ( u `' _E y <-> y e. u ) )
3 2 elv 
 |-  ( u `' _E y <-> y e. u )
4 3 anbi1ci 
 |-  ( ( u R x /\ u `' _E y ) <-> ( y e. u /\ u R x ) )
5 4 rexbii 
 |-  ( E. u e. A ( u R x /\ u `' _E y ) <-> E. u e. A ( y e. u /\ u R x ) )
6 5 opabbii 
 |-  { <. x , y >. | E. u e. A ( u R x /\ u `' _E y ) } = { <. x , y >. | E. u e. A ( y e. u /\ u R x ) }
7 1 6 eqtri 
 |-  ran ( R |X. ( `' _E |` A ) ) = { <. x , y >. | E. u e. A ( y e. u /\ u R x ) }