Metamath Proof Explorer


Theorem altxpeq2

Description: Equality for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012)

Ref Expression
Assertion altxpeq2 ( 𝐴 = 𝐵 → ( 𝐶 ×× 𝐴 ) = ( 𝐶 ×× 𝐵 ) )

Proof

Step Hyp Ref Expression
1 rexeq ( 𝐴 = 𝐵 → ( ∃ 𝑦𝐴 𝑧 = ⟪ 𝑥 , 𝑦 ⟫ ↔ ∃ 𝑦𝐵 𝑧 = ⟪ 𝑥 , 𝑦 ⟫ ) )
2 1 rexbidv ( 𝐴 = 𝐵 → ( ∃ 𝑥𝐶𝑦𝐴 𝑧 = ⟪ 𝑥 , 𝑦 ⟫ ↔ ∃ 𝑥𝐶𝑦𝐵 𝑧 = ⟪ 𝑥 , 𝑦 ⟫ ) )
3 2 abbidv ( 𝐴 = 𝐵 → { 𝑧 ∣ ∃ 𝑥𝐶𝑦𝐴 𝑧 = ⟪ 𝑥 , 𝑦 ⟫ } = { 𝑧 ∣ ∃ 𝑥𝐶𝑦𝐵 𝑧 = ⟪ 𝑥 , 𝑦 ⟫ } )
4 df-altxp ( 𝐶 ×× 𝐴 ) = { 𝑧 ∣ ∃ 𝑥𝐶𝑦𝐴 𝑧 = ⟪ 𝑥 , 𝑦 ⟫ }
5 df-altxp ( 𝐶 ×× 𝐵 ) = { 𝑧 ∣ ∃ 𝑥𝐶𝑦𝐵 𝑧 = ⟪ 𝑥 , 𝑦 ⟫ }
6 3 4 5 3eqtr4g ( 𝐴 = 𝐵 → ( 𝐶 ×× 𝐴 ) = ( 𝐶 ×× 𝐵 ) )