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