Theorem xpeq2i 5658

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

Syntax hints:   = wceq 1542   × cxp 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-opab 5148  df-xp 5637

This theorem is referenced by:  xpindir  5789  xpssres  5983  difxp1  6129  xpima  6146  xpexgALT  7934  curry1  8054  fparlem3  8064  fparlem4  8065  xp1en  9001  djuunxp  9845  dju1dif  10095  djuassen  10101  xpdjuen  10102  infdju1  10112  yonedalem3b  18245  yonedalem3  18246  pws1  20304  pwsmgp  20306  xkoinjcn  23652  imasdsf1olem  24338  df0op2  31823  ho01i  31899  nmop0h  32062  mbfmcst  34403  0rrv  34595  cvmlift2lem12  35496  zrdivrng  38274  funcsetc1o  49972