Theorem xpeq2i 5616

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 5610	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 × 𝐴) = (𝐶 × 𝐵)

Syntax hints:   = wceq 1539   × 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:  xpindir  5743  xpssres  5928  difxp1  6068  xpima  6085  xpexgALT  7824  curry1  7944  fparlem3  7954  fparlem4  7955  xp1en  8844  djuunxp  9679  dju1dif  9928  djuassen  9934  xpdjuen  9935  infdju1  9945  yonedalem3b  17997  yonedalem3  17998  pws1  19855  pwsmgp  19857  xkoinjcn  22838  imasdsf1olem  23526  df0op2  30114  ho01i  30190  nmop0h  30353  mbfmcst  32226  0rrv  32418  cvmlift2lem12  33276  zrdivrng  36111