Theorem xpeq2i 5712

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

Syntax hints:   = wceq 1540   × cxp 5683

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-opab 5206  df-xp 5691

This theorem is referenced by:  xpindir  5845  xpssres  6036  difxp1  6185  xpima  6202  xpexgALT  8006  curry1  8129  fparlem3  8139  fparlem4  8140  xp1en  9097  djuunxp  9961  dju1dif  10213  djuassen  10219  xpdjuen  10220  infdju1  10230  yonedalem3b  18324  yonedalem3  18325  pws1  20322  pwsmgp  20324  xkoinjcn  23695  imasdsf1olem  24383  df0op2  31771  ho01i  31847  nmop0h  32010  mbfmcst  34261  0rrv  34453  cvmlift2lem12  35319  zrdivrng  37960