Theorem xpeq2i 5707

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

Syntax hints:   = wceq 1533   × cxp 5678

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-sb 2060  df-clab 2705  df-cleq 2719  df-clel 2805  df-opab 5213  df-xp 5686

This theorem is referenced by:  xpindir  5839  xpssres  6025  difxp1  6172  xpima  6189  xpexgALT  7989  curry1  8113  fparlem3  8123  fparlem4  8124  xp1en  9086  djuunxp  9950  dju1dif  10201  djuassen  10207  xpdjuen  10208  infdju1  10218  yonedalem3b  18276  yonedalem3  18277  pws1  20266  pwsmgp  20268  xkoinjcn  23609  imasdsf1olem  24297  df0op2  31580  ho01i  31656  nmop0h  31819  mbfmcst  33884  0rrv  34076  cvmlift2lem12  34929  zrdivrng  37431