Theorem xpeq2i 5668

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

Syntax hints:   = wceq 1540   × cxp 5639

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-opab 5173  df-xp 5647

This theorem is referenced by:  xpindir  5801  xpssres  5992  difxp1  6141  xpima  6158  xpexgALT  7963  curry1  8086  fparlem3  8096  fparlem4  8097  xp1en  9031  djuunxp  9881  dju1dif  10133  djuassen  10139  xpdjuen  10140  infdju1  10150  yonedalem3b  18247  yonedalem3  18248  pws1  20241  pwsmgp  20243  xkoinjcn  23581  imasdsf1olem  24268  df0op2  31688  ho01i  31764  nmop0h  31927  mbfmcst  34257  0rrv  34449  cvmlift2lem12  35308  zrdivrng  37954  funcsetc1o  49490