Theorem xpeq2i 5649

Description: Equality inference for Cartesian product. (Contributed by NM, 21-Dec-2008.)

Hypothesis

Ref	Expression
xpeq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
xpeq2i	⊢ (𝐶 × 𝐴) = (𝐶 × 𝐵)

Proof of Theorem xpeq2i

Step	Hyp	Ref	Expression
1		xpeq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		xpeq2 5643	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 × 𝐴) = (𝐶 × 𝐵)

Syntax hints:   = wceq 1541   × cxp 5620

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 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-opab 5159  df-xp 5628

This theorem is referenced by:  xpindir  5781  xpssres  5975  difxp1  6121  xpima  6138  xpexgALT  7923  curry1  8044  fparlem3  8054  fparlem4  8055  xp1en  8989  djuunxp  9831  dju1dif  10081  djuassen  10087  xpdjuen  10088  infdju1  10098  yonedalem3b  18200  yonedalem3  18201  pws1  20258  pwsmgp  20260  xkoinjcn  23629  imasdsf1olem  24315  df0op2  31776  ho01i  31852  nmop0h  32015  mbfmcst  34365  0rrv  34557  cvmlift2lem12  35457  zrdivrng  38093  funcsetc1o  49684