Theorem xpeq2i 5682

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

This proof depends on syntax axioms:   = wceq 1570   × cxp 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-opab 5168  df-xp 5661

This theorem is used by:  xpindir  5814  xpssres  6011  difxp1  6157  xpima  6175  xpsnprg  7136  xpsntpg  7137  xpexgALT  7978  curry1  8101  fparlem3  8111  fparlem4  8112  xp1en  9061  djuunxp  9926  dju1dif  10175  djuassen  10181  xpdjuen  10182  infdju1  10192  yonedalem3b  18367  yonedalem3  18368  pws1  20465  pwsmgp  20467  xkoinjcn  23913  imasdsf1olem  24599  df0op2  32233  ho01i  32309  nmop0h  32472  mbfmcst  34770  0rrv  34962  cvmlift2lem12  35893  zrdivrng  38703  funcsetc1o  50423