Theorem xpeq1 5603

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 630	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
3	2	opabbidv 5140	. 2 ⊢ (𝐴 = 𝐵 → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)})
4		df-xp 5595	. 2 ⊢ (𝐴 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)}
5		df-xp 5595	. 2 ⊢ (𝐵 × 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)}
6	3, 4, 5	3eqtr4g 2803	1 ⊢ (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶))

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2106  {copab 5136   × cxp 5587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-opab 5137  df-xp 5595

This theorem is referenced by:  xpeq12  5614  xpeq1i  5615  xpeq1d  5618  opthprc  5651  dmxpid  5839  reseq2  5886  xpnz  6062  xpdisj1  6064  xpcan2  6080  xpima  6085  unixp  6185  unixpid  6187  pmvalg  8626  xpsneng  8843  xpcomeng  8851  xpdom2g  8855  fodomr  8915  unxpdom  9030  xpfi  9085  marypha1lem  9192  iundom2g  10296  hashxplem  14148  dmtrclfv  14729  ramcl  16730  efgval  19323  frgpval  19364  frlmval  20955  txuni2  22716  txbas  22718  txopn  22753  txrest  22782  txdis  22783  txdis1cn  22786  tx1stc  22801  tmdgsum  23246  qustgplem  23272  incistruhgr  27449  isgrpo  28859  hhssablo  29625  hhssnvt  29627  hhsssh  29631  gsumpart  31315  txomap  31784  tpr2rico  31862  elsx  32162  br2base  32236  dya2iocnrect  32248  sxbrsigalem5  32255  sibf0  32301  cvmlift2lem13  33277  naddcllem  33831