Theorem xpeq1 5571

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 2903	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	anbi1d 631	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
3	2	opabbidv 5134	. 2 ⊢ (𝐴 = 𝐵 → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)})
4		df-xp 5563	. 2 ⊢ (𝐴 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)}
5		df-xp 5563	. 2 ⊢ (𝐵 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)}
6	3, 4, 5	3eqtr4g 2883	1 ⊢ (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶))

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114  {copab 5130   × cxp 5555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-opab 5131  df-xp 5563

This theorem is referenced by:  xpeq12  5582  xpeq1i  5583  xpeq1d  5586  opthprc  5618  dmxpid  5802  reseq2  5850  xpnz  6018  xpdisj1  6020  xpcan2  6036  xpima  6041  unixp  6135  unixpid  6137  pmvalg  8419  xpsneng  8604  xpcomeng  8611  xpdom2g  8615  fodomr  8670  unxpdom  8727  xpfi  8791  marypha1lem  8899  iundom2g  9964  hashxplem  13797  dmtrclfv  14380  ramcl  16367  efgval  18845  frgpval  18886  frlmval  20894  txuni2  22175  txbas  22177  txopn  22212  txrest  22241  txdis  22242  txdis1cn  22245  tx1stc  22260  tmdgsum  22705  qustgplem  22731  incistruhgr  26866  isgrpo  28276  hhssablo  29042  hhssnvt  29044  hhsssh  29048  txomap  31100  tpr2rico  31157  elsx  31455  br2base  31529  dya2iocnrect  31541  sxbrsigalem5  31548  sibf0  31594  cvmlift2lem13  32564