Theorem xpeq1 5675

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  {copab 5173   × cxp 5659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-opab 5174  df-xp 5667

This theorem is referenced by:  xpeq12  5686  xpeq1i  5687  xpeq1d  5690  opthprc  5725  dmxpid  5920  reseq2  5973  xpnz  6156  xpdisj1  6158  xpcan2  6175  xpima  6180  unixp  6283  unixpid  6285  naddcllem  8658  pmvalg  8830  xpsneng  9046  xpcomeng  9053  xpdom2g  9057  fodomr  9112  unxpdom  9215  fodomfir  9283  marypha1lem  9389  iundom2g  10519  hashxplem  14466  dmtrclfv  15051  ramcl  17084  efgval  19782  frgpval  19823  frlmval  21898  txuni2  23722  txbas  23724  txopn  23759  txrest  23788  txdis  23789  txdis1cn  23792  tx1stc  23807  tmdgsum  24252  qustgplem  24278  incistruhgr  29429  isgrpo  30849  hhssablo  31615  hhssnvt  31617  hhsssh  31621  gsumpart  33383  txomap  34224  tpr2rico  34302  elsx  34584  br2base  34659  dya2iocnrect  34671  sxbrsigalem5  34678  sibf0  34724  cvmlift2lem13  35807