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

Metamath Proof Explorer

Theorem rnxrnidres

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

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

Proof

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