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	⊢ ( 𝐴 ∈ 𝑉 → [ 𝐴 ] ( 𝑅 ⋉ ◡ E ) = ( [ 𝐴 ] 𝑅 × 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ecxrn2	⊢ ( 𝐴 ∈ 𝑉 → [ 𝐴 ] ( 𝑅 ⋉ ◡ E ) = ( [ 𝐴 ] 𝑅 × [ 𝐴 ] ◡ E ) )
2		eccnvep	⊢ ( 𝐴 ∈ 𝑉 → [ 𝐴 ] ◡ E = 𝐴 )
3	2	xpeq2d	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 ] 𝑅 × [ 𝐴 ] ◡ E ) = ( [ 𝐴 ] 𝑅 × 𝐴 ) )
4	1 3	eqtrd	⊢ ( 𝐴 ∈ 𝑉 → [ 𝐴 ] ( 𝑅 ⋉ ◡ E ) = ( [ 𝐴 ] 𝑅 × 𝐴 ) )