Metamath Proof Explorer

Theorem bj-xtageq

Description: The products of a given class and the tagging of either of two equal classes are equal. (Contributed by BJ, 6-Apr-2019)

Ref Expression
Assertion bj-xtageq 
|- ( A = B -> ( C X. tag A ) = ( C X. tag B ) )

Proof

Step Hyp Ref Expression
1 bj-tageq 
 |-  ( A = B -> tag A = tag B )
2 1 xpeq2d 
 |-  ( A = B -> ( C X. tag A ) = ( C X. tag B ) )