Theorem xpeq2i 5645

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

Syntax hints:   = wceq 1547   × cxp 5616

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-opab 5135  df-xp 5624

This theorem is referenced by:  xpindir  5776  xpssres  5970  difxp1  6116  xpima  6133  xpexgALT  7923  curry1  8043  fparlem3  8053  fparlem4  8054  xp1en  8991  djuunxp  9836  dju1dif  10086  djuassen  10092  xpdjuen  10093  infdju1  10103  yonedalem3b  18236  yonedalem3  18237  pws1  20295  pwsmgp  20297  xkoinjcn  23670  imasdsf1olem  24356  df0op2  31841  ho01i  31917  nmop0h  32080  mbfmcst  34443  0rrv  34635  cvmlift2lem12  35542  zrdivrng  38320  funcsetc1o  49987