Theorem xpeq2i 5641

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

Syntax hints:   = wceq 1541   × cxp 5612

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-opab 5152  df-xp 5620

This theorem is referenced by:  xpindir  5773  xpssres  5966  difxp1  6112  xpima  6129  xpexgALT  7913  curry1  8034  fparlem3  8044  fparlem4  8045  xp1en  8976  djuunxp  9814  dju1dif  10064  djuassen  10070  xpdjuen  10071  infdju1  10081  yonedalem3b  18185  yonedalem3  18186  pws1  20243  pwsmgp  20245  xkoinjcn  23602  imasdsf1olem  24288  df0op2  31732  ho01i  31808  nmop0h  31971  mbfmcst  34272  0rrv  34464  cvmlift2lem12  35358  zrdivrng  38001  funcsetc1o  49537