Theorem xpeq1 5625

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111  {copab 5148   × cxp 5609

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-opab 5149  df-xp 5617

This theorem is referenced by:  xpeq12  5636  xpeq1i  5637  xpeq1d  5640  opthprc  5675  dmxpid  5865  reseq2  5918  xpnz  6101  xpdisj1  6103  xpcan2  6119  xpima  6124  unixp  6224  unixpid  6226  naddcllem  8586  pmvalg  8756  xpsneng  8970  xpcomeng  8977  xpdom2g  8981  fodomr  9036  unxpdom  9138  fodomfir  9207  marypha1lem  9312  iundom2g  10426  hashxplem  14335  dmtrclfv  14920  ramcl  16936  efgval  19624  frgpval  19665  frlmval  21680  txuni2  23475  txbas  23477  txopn  23512  txrest  23541  txdis  23542  txdis1cn  23545  tx1stc  23560  tmdgsum  24005  qustgplem  24031  incistruhgr  29052  isgrpo  30469  hhssablo  31235  hhssnvt  31237  hhsssh  31241  gsumpart  33029  txomap  33839  tpr2rico  33917  elsx  34199  br2base  34274  dya2iocnrect  34286  sxbrsigalem5  34293  sibf0  34339  cvmlift2lem13  35351