Theorem xpeq2i 5690

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

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

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-opab 5176  df-xp 5669

This theorem is used by:  xpindir  5822  xpssres  6019  difxp1  6164  xpima  6182  xpsnprg  7142  xpsntpg  7143  xpexgALT  7984  curry1  8105  fparlem3  8115  fparlem4  8116  xp1en  9058  djuunxp  9923  dju1dif  10172  djuassen  10178  xpdjuen  10179  infdju1  10189  yonedalem3b  18357  yonedalem3  18358  pws1  20452  pwsmgp  20454  xkoinjcn  23895  imasdsf1olem  24581  df0op2  32175  ho01i  32251  nmop0h  32414  mbfmcst  34714  0rrv  34906  cvmlift2lem12  35843  zrdivrng  38662  funcsetc1o  50332