Theorem xpeq2i 5607

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

Syntax hints:   = wceq 1539   × cxp 5578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-opab 5133  df-xp 5586

This theorem is referenced by:  xpindir  5732  xpssres  5917  difxp1  6057  xpima  6074  xpexgALT  7797  curry1  7915  fparlem3  7925  fparlem4  7926  xp1en  8798  djuunxp  9610  dju1dif  9859  djuassen  9865  xpdjuen  9866  infdju1  9876  yonedalem3b  17913  yonedalem3  17914  pws1  19770  pwsmgp  19772  xkoinjcn  22746  imasdsf1olem  23434  df0op2  30015  ho01i  30091  nmop0h  30254  mbfmcst  32126  0rrv  32318  cvmlift2lem12  33176  zrdivrng  36038