Theorem xpeq1 5604

Description: Equality theorem for Cartesian product. (Contributed by NM, 4-Jul-1994.)

Assertion

Ref	Expression
xpeq1	⊢ (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶))

Proof of Theorem xpeq1

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq2 2829	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	anbi1d 630	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
3	2	opabbidv 5145	. 2 ⊢ (𝐴 = 𝐵 → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)})
4		df-xp 5596	. 2 ⊢ (𝐴 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)}
5		df-xp 5596	. 2 ⊢ (𝐵 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)}
6	3, 4, 5	3eqtr4g 2805	1 ⊢ (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶))

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1542   ∈ wcel 2110  {copab 5141   × cxp 5588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-opab 5142  df-xp 5596

This theorem is referenced by:  xpeq12  5615  xpeq1i  5616  xpeq1d  5619  opthprc  5652  dmxpid  5838  reseq2  5885  xpnz  6061  xpdisj1  6063  xpcan2  6079  xpima  6084  unixp  6184  unixpid  6186  pmvalg  8609  xpsneng  8826  xpcomeng  8833  xpdom2g  8837  fodomr  8897  unxpdom  9008  xpfi  9063  marypha1lem  9170  iundom2g  10297  hashxplem  14146  dmtrclfv  14727  ramcl  16728  efgval  19321  frgpval  19362  frlmval  20953  txuni2  22714  txbas  22716  txopn  22751  txrest  22780  txdis  22781  txdis1cn  22784  tx1stc  22799  tmdgsum  23244  qustgplem  23270  incistruhgr  27447  isgrpo  28855  hhssablo  29621  hhssnvt  29623  hhsssh  29627  gsumpart  31311  txomap  31780  tpr2rico  31858  elsx  32158  br2base  32232  dya2iocnrect  32244  sxbrsigalem5  32251  sibf0  32297  cvmlift2lem13  33273  naddcllem  33827