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

Metamath Proof Explorer

Theorem ecxrncnvep

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

		Ref	Expression
	Assertion	ecxrncnvep	$⊢ A \in V \to [A] R ⋉ E^{-1} = \{⟨y, z⟩ \| (z \in A \land A R y)\}$

Step	Hyp	Ref	Expression
1		ecxrn	$⊢ A \in V \to [A] R ⋉ E^{-1} = \{⟨y, z⟩ \| (A R y \land A E^{-1} z)\}$
2		brcnvep	$⊢ A \in V \to (A E^{-1} z \leftrightarrow z \in A)$
3	2	anbi1cd	$⊢ A \in V \to ((A R y \land A E^{-1} z) \leftrightarrow (z \in A \land A R y))$
4	3	opabbidv	$⊢ A \in V \to \{⟨y, z⟩ \| (A R y \land A E^{-1} z)\} = \{⟨y, z⟩ \| (z \in A \land A R y)\}$
5	1 4	eqtrd	$⊢ A \in V \to [A] R ⋉ E^{-1} = \{⟨y, z⟩ \| (z \in A \land A R y)\}$