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 \left[A\right]R⋉{\mathrm{E}}^{-1}=\left\{⟨y,z⟩|\left(z\in A\wedge ARy\right)\right\}$$

Proof

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