Theorem xpeq2i 5716

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

Syntax hints:   = wceq 1537   × cxp 5687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-opab 5211  df-xp 5695

This theorem is referenced by:  xpindir  5848  xpssres  6038  difxp1  6187  xpima  6204  xpexgALT  8005  curry1  8128  fparlem3  8138  fparlem4  8139  xp1en  9096  djuunxp  9959  dju1dif  10211  djuassen  10217  xpdjuen  10218  infdju1  10228  yonedalem3b  18336  yonedalem3  18337  pws1  20339  pwsmgp  20341  xkoinjcn  23711  imasdsf1olem  24399  df0op2  31781  ho01i  31857  nmop0h  32020  mbfmcst  34241  0rrv  34433  cvmlift2lem12  35299  zrdivrng  37940