Theorem ecxrncnvep2

Description: The ( R |X.`' _E ) -coset of a set is the Cartesian product of its R ` -coset and the set. (Contributed by Peter Mazsa, 25-Jan-2026)

	Ref	Expression
Assertion	ecxrncnvep2	$$⊢A\in V\to \left[A\right]R⋉{\mathrm{E}}^{-1}=\left[A\right]R\times A$$

Proof

Step	Hyp	Ref	Expression
1		ecxrn2	$$⊢A\in V\to \left[A\right]R⋉{\mathrm{E}}^{-1}=\left[A\right]R\times \left[A\right]{\mathrm{E}}^{-1}$$
2		eccnvep	$$⊢A\in V\to \left[A\right]{\mathrm{E}}^{-1}=A$$
3	2	xpeq2d	$$⊢A\in V\to \left[A\right]R\times \left[A\right]{\mathrm{E}}^{-1}=\left[A\right]R\times A$$
4	1 3	eqtrd	$$⊢A\in V\to \left[A\right]R⋉{\mathrm{E}}^{-1}=\left[A\right]R\times A$$