Theorem xpeq1 5657

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559   ∈ wcel 2141  {copab 5159   × cxp 5641

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-opab 5160  df-xp 5649

This theorem is referenced by:  xpeq12  5668  xpeq1i  5669  xpeq1d  5672  opthprc  5707  dmxpid  5902  reseq2  5956  xpnz  6140  xpdisj1  6142  xpcan2  6158  xpima  6163  unixp  6264  unixpid  6266  naddcllem  8640  pmvalg  8812  xpsneng  9028  xpcomeng  9035  xpdom2g  9039  fodomr  9094  unxpdom  9197  fodomfir  9266  marypha1lem  9373  iundom2g  10491  hashxplem  14440  dmtrclfv  15025  ramcl  17056  efgval  19748  frgpval  19789  frlmval  21788  txuni2  23613  txbas  23615  txopn  23650  txrest  23679  txdis  23680  txdis1cn  23683  tx1stc  23698  tmdgsum  24143  qustgplem  24169  incistruhgr  29237  isgrpo  30657  hhssablo  31423  hhssnvt  31425  hhsssh  31429  gsumpart  33204  txomap  34092  tpr2rico  34170  elsx  34452  br2base  34527  dya2iocnrect  34539  sxbrsigalem5  34546  sibf0  34592  cvmlift2lem13  35626