Description: Equality for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012)
Ref | Expression | ||
---|---|---|---|
Assertion | altxpeq2 | ⊢ ( 𝐴 = 𝐵 → ( 𝐶 ×× 𝐴 ) = ( 𝐶 ×× 𝐵 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexeq | ⊢ ( 𝐴 = 𝐵 → ( ∃ 𝑦 ∈ 𝐴 𝑧 = ⟪ 𝑥 , 𝑦 ⟫ ↔ ∃ 𝑦 ∈ 𝐵 𝑧 = ⟪ 𝑥 , 𝑦 ⟫ ) ) | |
2 | 1 | rexbidv | ⊢ ( 𝐴 = 𝐵 → ( ∃ 𝑥 ∈ 𝐶 ∃ 𝑦 ∈ 𝐴 𝑧 = ⟪ 𝑥 , 𝑦 ⟫ ↔ ∃ 𝑥 ∈ 𝐶 ∃ 𝑦 ∈ 𝐵 𝑧 = ⟪ 𝑥 , 𝑦 ⟫ ) ) |
3 | 2 | abbidv | ⊢ ( 𝐴 = 𝐵 → { 𝑧 ∣ ∃ 𝑥 ∈ 𝐶 ∃ 𝑦 ∈ 𝐴 𝑧 = ⟪ 𝑥 , 𝑦 ⟫ } = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐶 ∃ 𝑦 ∈ 𝐵 𝑧 = ⟪ 𝑥 , 𝑦 ⟫ } ) |
4 | df-altxp | ⊢ ( 𝐶 ×× 𝐴 ) = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐶 ∃ 𝑦 ∈ 𝐴 𝑧 = ⟪ 𝑥 , 𝑦 ⟫ } | |
5 | df-altxp | ⊢ ( 𝐶 ×× 𝐵 ) = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐶 ∃ 𝑦 ∈ 𝐵 𝑧 = ⟪ 𝑥 , 𝑦 ⟫ } | |
6 | 3 4 5 | 3eqtr4g | ⊢ ( 𝐴 = 𝐵 → ( 𝐶 ×× 𝐴 ) = ( 𝐶 ×× 𝐵 ) ) |