This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 \in V \to Rel [A] R ⋉ S$

Step	Hyp	Ref	Expression
1		relopab	$⊢ Rel \{⟨y, z⟩ \| (A R y \land A S z)\}$
2		ecxrn	$⊢ A \in V \to [A] R ⋉ S = \{⟨y, z⟩ \| (A R y \land A S z)\}$
3	2	releqd	$⊢ A \in V \to (Rel [A] R ⋉ S \leftrightarrow Rel \{⟨y, z⟩ \| (A R y \land A S z)\})$
4	1 3	mpbiri	$⊢ A \in V \to Rel [A] R ⋉ S$