Theorem xpeq2i 5553

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

Syntax hints:   = wceq 1542   × cxp 5524

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 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-opab 5094  df-xp 5532

This theorem is referenced by:  xpindir  5678  xpssres  5863  difxp1  5998  xpima  6015  xpexgALT  7708  curry1  7826  fparlem3  7836  fparlem4  7837  xp1en  8653  djuunxp  9424  dju1dif  9673  djuassen  9679  xpdjuen  9680  infdju1  9690  yonedalem3b  17646  yonedalem3  17647  pws1  19489  pwsmgp  19491  xkoinjcn  22439  imasdsf1olem  23127  df0op2  29687  ho01i  29763  nmop0h  29926  mbfmcst  31796  0rrv  31988  cvmlift2lem12  32847  zrdivrng  35731