Theorem xpeq1 5702

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536   ∈ wcel 2105  {copab 5209   × cxp 5686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-opab 5210  df-xp 5694

This theorem is referenced by:  xpeq12  5713  xpeq1i  5714  xpeq1d  5717  opthprc  5752  dmxpid  5943  reseq2  5994  xpnz  6180  xpdisj1  6182  xpcan2  6198  xpima  6203  unixp  6303  unixpid  6305  naddcllem  8712  pmvalg  8875  xpsneng  9094  xpcomeng  9102  xpdom2g  9106  fodomr  9166  unxpdom  9286  xpfiOLD  9356  fodomfir  9365  marypha1lem  9470  iundom2g  10577  hashxplem  14468  dmtrclfv  15053  ramcl  17062  efgval  19749  frgpval  19790  frlmval  21785  txuni2  23588  txbas  23590  txopn  23625  txrest  23654  txdis  23655  txdis1cn  23658  tx1stc  23673  tmdgsum  24118  qustgplem  24144  incistruhgr  29110  isgrpo  30525  hhssablo  31291  hhssnvt  31293  hhsssh  31297  gsumpart  33042  txomap  33794  tpr2rico  33872  elsx  34174  br2base  34250  dya2iocnrect  34262  sxbrsigalem5  34269  sibf0  34315  cvmlift2lem13  35299