Description: Equality deduction for a Cartesian square, see Wikipedia "Cartesian product", https://en.wikipedia.org/wiki/Cartesian_product#n-ary_Cartesian_power . (Contributed by AV, 13-Jan-2020)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | xpeq1d.1 | |- ( ph -> A = B ) |
|
| Assertion | sqxpeqd | |- ( ph -> ( A X. A ) = ( B X. B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | xpeq1d.1 | |- ( ph -> A = B ) |
|
| 2 | 1 1 | xpeq12d | |- ( ph -> ( A X. A ) = ( B X. B ) ) |