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	⊢ ( 𝐴 ∈ 𝑉 → Rel [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		relopab	⊢ Rel { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝐴 𝑅 𝑦 ∧ 𝐴 𝑆 𝑧 ) }
2		ecxrn	⊢ ( 𝐴 ∈ 𝑉 → [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝐴 𝑅 𝑦 ∧ 𝐴 𝑆 𝑧 ) } )
3	2	releqd	⊢ ( 𝐴 ∈ 𝑉 → ( Rel [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) ↔ Rel { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝐴 𝑅 𝑦 ∧ 𝐴 𝑆 𝑧 ) } ) )
4	1 3	mpbiri	⊢ ( 𝐴 ∈ 𝑉 → Rel [ 𝐴 ] ( 𝑅 ⋉ 𝑆 ) )