Theorem xpeq2i 5646

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

Syntax hints:   = wceq 1540   × cxp 5617

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 5155  df-xp 5625

This theorem is referenced by:  xpindir  5777  xpssres  5969  difxp1  6114  xpima  6131  xpexgALT  7916  curry1  8037  fparlem3  8047  fparlem4  8048  xp1en  8980  djuunxp  9817  dju1dif  10067  djuassen  10073  xpdjuen  10074  infdju1  10084  yonedalem3b  18185  yonedalem3  18186  pws1  20210  pwsmgp  20212  xkoinjcn  23572  imasdsf1olem  24259  df0op2  31696  ho01i  31772  nmop0h  31935  mbfmcst  34227  0rrv  34419  cvmlift2lem12  35287  zrdivrng  37933  funcsetc1o  49482