Theorem xpeq1 5652

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  {copab 5172   × cxp 5636

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-opab 5173  df-xp 5644

This theorem is referenced by:  xpeq12  5663  xpeq1i  5664  xpeq1d  5667  opthprc  5701  dmxpid  5890  reseq2  5937  xpnz  6116  xpdisj1  6118  xpcan2  6134  xpima  6139  unixp  6239  unixpid  6241  naddcllem  8627  pmvalg  8783  xpsneng  9007  xpcomeng  9015  xpdom2g  9019  fodomr  9079  unxpdom  9204  xpfiOLD  9269  marypha1lem  9378  iundom2g  10485  hashxplem  14343  dmtrclfv  14915  ramcl  16912  efgval  19513  frgpval  19554  frlmval  21191  txuni2  22953  txbas  22955  txopn  22990  txrest  23019  txdis  23020  txdis1cn  23023  tx1stc  23038  tmdgsum  23483  qustgplem  23509  incistruhgr  28093  isgrpo  29502  hhssablo  30268  hhssnvt  30270  hhsssh  30274  gsumpart  31967  txomap  32504  tpr2rico  32582  elsx  32882  br2base  32958  dya2iocnrect  32970  sxbrsigalem5  32977  sibf0  33023  cvmlift2lem13  33996