Theorem ecxrncnvep

Description: The ( R |X.`' _E ) ` -coset of a set. (Contributed by Peter Mazsa, 22-May-2021)

	Ref	Expression
Assertion	ecxrncnvep	|- ( A e. V -> [ A ] ( R |X. `' _E ) = { <. y , z >. | ( z e. A /\ A R y ) } )

Proof

Step	Hyp	Ref	Expression
1		ecxrn	|- ( A e. V -> [ A ] ( R |X. `' _E ) = { <. y , z >. | ( A R y /\ A `' _E z ) } )
2		brcnvep	|- ( A e. V -> ( A `' _E z <-> z e. A ) )
3	2	anbi1cd	|- ( A e. V -> ( ( A R y /\ A `' _E z ) <-> ( z e. A /\ A R y ) ) )
4	3	opabbidv	|- ( A e. V -> { <. y , z >. | ( A R y /\ A `' _E z ) } = { <. y , z >. | ( z e. A /\ A R y ) } )
5	1 4	eqtrd	|- ( A e. V -> [ A ] ( R |X. `' _E ) = { <. y , z >. | ( z e. A /\ A R y ) } )