Theorem xpeq2i 5652

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

Syntax hints:   = wceq 1542   × cxp 5623

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-opab 5149  df-xp 5631

This theorem is referenced by:  xpindir  5784  xpssres  5978  difxp1  6124  xpima  6141  xpexgALT  7928  curry1  8048  fparlem3  8058  fparlem4  8059  xp1en  8995  djuunxp  9839  dju1dif  10089  djuassen  10095  xpdjuen  10096  infdju1  10106  yonedalem3b  18239  yonedalem3  18240  pws1  20298  pwsmgp  20300  xkoinjcn  23665  imasdsf1olem  24351  df0op2  31841  ho01i  31917  nmop0h  32080  mbfmcst  34422  0rrv  34614  cvmlift2lem12  35515  zrdivrng  38291  funcsetc1o  49987