Theorem xpeq2i 5651

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

Syntax hints:   = wceq 1541   × cxp 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-opab 5161  df-xp 5630

This theorem is referenced by:  xpindir  5783  xpssres  5977  difxp1  6123  xpima  6140  xpexgALT  7925  curry1  8046  fparlem3  8056  fparlem4  8057  xp1en  8991  djuunxp  9833  dju1dif  10083  djuassen  10089  xpdjuen  10090  infdju1  10100  yonedalem3b  18202  yonedalem3  18203  pws1  20260  pwsmgp  20262  xkoinjcn  23631  imasdsf1olem  24317  df0op2  31827  ho01i  31903  nmop0h  32066  mbfmcst  34416  0rrv  34608  cvmlift2lem12  35508  zrdivrng  38154  funcsetc1o  49742