Theorem xpeq2i 5678

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

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

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-opab 5168  df-xp 5657

This theorem is used by:  xpindir  5811  xpssres  6007  difxp1  6156  xpima  6174  xpsnprg  7141  xpsntpg  7142  xpexgALT  7991  curry1  8113  fparlem3  8123  fparlem4  8124  xp1en  9075  djuunxp  9995  dju1dif  10244  djuassen  10250  xpdjuen  10251  infdju1  10261  yonedalem3b  18446  yonedalem3  18447  pws1  20547  pwsmgp  20549  xkoinjcn  23999  imasdsf1olem  24685  df0op2  32347  ho01i  32423  nmop0h  32586  mbfmcst  34884  0rrv  35076  cvmlift2lem12  36058  zrdivrng  38867  funcsetc1o  50574