Theorem xpeq2i 5665

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

Syntax hints:   = wceq 1540   × cxp 5636

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-opab 5170  df-xp 5644

This theorem is referenced by:  xpindir  5798  xpssres  5989  difxp1  6138  xpima  6155  xpexgALT  7960  curry1  8083  fparlem3  8093  fparlem4  8094  xp1en  9027  djuunxp  9874  dju1dif  10126  djuassen  10132  xpdjuen  10133  infdju1  10143  yonedalem3b  18240  yonedalem3  18241  pws1  20234  pwsmgp  20236  xkoinjcn  23574  imasdsf1olem  24261  df0op2  31681  ho01i  31757  nmop0h  31920  mbfmcst  34250  0rrv  34442  cvmlift2lem12  35301  zrdivrng  37947  funcsetc1o  49486