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 e. V -> [ A ] ( R |X. `' _E ) = ( [ A ] R X. A ) )

Proof

Step Hyp Ref Expression
1 ecxrn2 
 |-  ( A e. V -> [ A ] ( R |X. `' _E ) = ( [ A ] R X. [ A ] `' _E ) )
2 eccnvep 
 |-  ( A e. V -> [ A ] `' _E = A )
3 2 xpeq2d 
 |-  ( A e. V -> ( [ A ] R X. [ A ] `' _E ) = ( [ A ] R X. A ) )
4 1 3 eqtrd 
 |-  ( A e. V -> [ A ] ( R |X. `' _E ) = ( [ A ] R X. A ) )