Theorem xpeq2i 5678

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

This proof depends on syntax axioms:   = wceq 1569   × cxp 5649

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-opab 5167  df-xp 5657

This theorem is used by:  xpindir  5812  xpssres  6009  difxp1  6158  xpima  6176  xpsnprg  7148  xpsntpg  7149  xpexgALT  7997  curry1  8121  fparlem3  8131  fparlem4  8132  xp1en  9089  djuunxp  10009  dju1dif  10258  djuassen  10264  xpdjuen  10265  infdju1  10275  yonedalem3b  18462  yonedalem3  18463  pws1  20563  pwsmgp  20565  xkoinjcn  24015  imasdsf1olem  24701  df0op2  32363  ho01i  32439  nmop0h  32602  mbfmcst  34941  0rrv  35133  cvmlift2lem12  36169  zrdivrng  38996  funcsetc1o  50740