Theorem xpeq2i 5659

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

Syntax hints:   = wceq 1542   × cxp 5630

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-opab 5163  df-xp 5638

This theorem is referenced by:  xpindir  5791  xpssres  5985  difxp1  6131  xpima  6148  xpexgALT  7935  curry1  8056  fparlem3  8066  fparlem4  8067  xp1en  9003  djuunxp  9845  dju1dif  10095  djuassen  10101  xpdjuen  10102  infdju1  10112  yonedalem3b  18214  yonedalem3  18215  pws1  20272  pwsmgp  20274  xkoinjcn  23643  imasdsf1olem  24329  df0op2  31840  ho01i  31916  nmop0h  32079  mbfmcst  34437  0rrv  34629  cvmlift2lem12  35530  zrdivrng  38204  funcsetc1o  49856