Theorem xpeq1 5677

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  {copab 5175   × cxp 5661

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-opab 5176  df-xp 5669

This theorem is used by:  xpeq12  5688  xpeq1i  5689  xpeq1d  5692  opthprc  5727  dmxpid  5922  reseq2  5975  xpnz  6158  xpdisj1  6160  xpcan2  6177  xpima  6182  unixp  6287  unixpid  6289  naddcllem  8668  pmvalg  8840  xpsneng  9057  xpcomeng  9064  xpdom2g  9068  fodomr  9123  unxpdom  9226  fodomfir  9294  marypha1lem  9400  iundom2g  10539  hashxplem  14488  dmtrclfv  15079  ramcl  17111  efgval  19831  frgpval  19872  frlmval  21948  txuni2  23773  txbas  23775  txopn  23810  txrest  23839  txdis  23840  txdis1cn  23843  tx1stc  23858  tmdgsum  24303  qustgplem  24329  incistruhgr  29484  isgrpo  30920  hhssablo  31686  hhssnvt  31688  hhsssh  31692  gsumpart  33447  txomap  34288  tpr2rico  34366  elsx  34649  br2base  34724  dya2iocnrect  34736  sxbrsigalem5  34743  sibf0  34789  cvmlift2lem13  35844