Theorem xpeq2i 5546

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

Syntax hints:   = wceq 1538   × cxp 5517

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-opab 5093  df-xp 5525

This theorem is referenced by:  xpindir  5669  xpssres  5855  difxp1  5989  xpima  6006  xpexgALT  7664  curry1  7782  fparlem3  7792  fparlem4  7793  xp1en  8586  djuunxp  9334  dju1dif  9583  djuassen  9589  xpdjuen  9590  infdju1  9600  yonedalem3b  17521  yonedalem3  17522  pws1  19362  pwsmgp  19364  xkoinjcn  22292  imasdsf1olem  22980  df0op2  29535  ho01i  29611  nmop0h  29774  mbfmcst  31627  0rrv  31819  cvmlift2lem12  32674  zrdivrng  35391