Theorem relecxrn

Description: The ( R |X. S ) -coset of a set is a relation. (Contributed by Peter Mazsa, 15-Oct-2020)

	Ref	Expression
Assertion	relecxrn	|- ( A e. V -> Rel [ A ] ( R |X. S ) )

Proof

Step	Hyp	Ref	Expression
1		relopab	|- Rel { <. y , z >. | ( A R y /\ A S z ) }
2		ecxrn	|- ( A e. V -> [ A ] ( R |X. S ) = { <. y , z >. | ( A R y /\ A S z ) } )
3	2	releqd	|- ( A e. V -> ( Rel [ A ] ( R |X. S ) <-> Rel { <. y , z >. | ( A R y /\ A S z ) } ) )
4	1 3	mpbiri	|- ( A e. V -> Rel [ A ] ( R |X. S ) )