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 ) }