Theorem xpeq2i 5582

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

Syntax hints:   = wceq 1537   × cxp 5553

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-opab 5129  df-xp 5561

This theorem is referenced by:  xpindir  5705  xpssres  5889  difxp1  6022  xpima  6039  xpexgALT  7682  curry1  7799  fparlem3  7809  fparlem4  7810  xp1en  8603  djuunxp  9350  dju1dif  9598  djuassen  9604  xpdjuen  9605  infdju1  9615  yonedalem3b  17529  yonedalem3  17530  pws1  19366  pwsmgp  19368  xkoinjcn  22295  imasdsf1olem  22983  df0op2  29529  ho01i  29605  nmop0h  29768  mbfmcst  31517  0rrv  31709  cvmlift2lem12  32561  zrdivrng  35246