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

Metamath Proof Explorer

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 [A] R ⋉ E^{-1} = [A] R \times A$

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