Theorem xpeq2i 5703

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

Syntax hints:   = wceq 1541   × cxp 5674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-opab 5211  df-xp 5682

This theorem is referenced by:  xpindir  5834  xpssres  6018  difxp1  6164  xpima  6181  xpexgALT  7970  curry1  8092  fparlem3  8102  fparlem4  8103  xp1en  9059  djuunxp  9918  dju1dif  10169  djuassen  10175  xpdjuen  10176  infdju1  10186  yonedalem3b  18236  yonedalem3  18237  pws1  20213  pwsmgp  20215  xkoinjcn  23411  imasdsf1olem  24099  df0op2  31260  ho01i  31336  nmop0h  31499  mbfmcst  33544  0rrv  33736  cvmlift2lem12  34591  zrdivrng  37124