Theorem xpeq2i 5688

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

Syntax hints:   = wceq 1570   × cxp 5659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-opab 5174  df-xp 5667

This theorem is referenced by:  xpindir  5820  xpssres  6017  difxp1  6162  xpima  6180  xpexgALT  7974  curry1  8095  fparlem3  8105  fparlem4  8106  xp1en  9047  djuunxp  9903  dju1dif  10152  djuassen  10158  xpdjuen  10159  infdju1  10169  yonedalem3b  18330  yonedalem3  18331  pws1  20402  pwsmgp  20404  xkoinjcn  23844  imasdsf1olem  24530  df0op2  32104  ho01i  32180  nmop0h  32343  mbfmcst  34649  0rrv  34841  cvmlift2lem12  35806  zrdivrng  38604  funcsetc1o  50275