Theorem xpeq2i 5060

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

Syntax hints:   = wceq 1475   × cxp 5036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-opab 4644  df-xp 5044

This theorem is referenced by:  xpindir  5178  xpssres  5354  difxp1  5478  xpima  5495  xpexgALT  7052  curry1  7156  fparlem3  7166  fparlem4  7167  xp1en  7931  xp2cda  8885  xpcdaen  8888  pwcda1  8899  pwcdandom  9368  yonedalem3b  16742  yonedalem3  16743  pws1  18439  pwsmgp  18441  xkoinjcn  21300  imasdsf1olem  21988  df0op2  27995  ho01i  28071  nmop0h  28234  mbfmcst  29648  0rrv  29840  cvmlift2lem12  30550  zrdivrng  32922