Theorem xpeq2i 5674

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

Syntax hints:   = wceq 1560   × cxp 5645

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-opab 5163  df-xp 5653

This theorem is referenced by:  xpindir  5806  xpssres  6004  difxp1  6150  xpima  6168  xpexgALT  7962  curry1  8083  fparlem3  8093  fparlem4  8094  xp1en  9035  djuunxp  9879  dju1dif  10129  djuassen  10135  xpdjuen  10136  infdju1  10146  yonedalem3b  18311  yonedalem3  18312  pws1  20369  pwsmgp  20371  xkoinjcn  23744  imasdsf1olem  24430  df0op2  31952  ho01i  32028  nmop0h  32191  mbfmcst  34553  0rrv  34745  cvmlift2lem12  35661  zrdivrng  38449  funcsetc1o  50115