Theorem xpeq2i 5584

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

Syntax hints:   = wceq 1537   × cxp 5555

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 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-opab 5131  df-xp 5563

This theorem is referenced by:  xpindir  5707  xpssres  5891  difxp1  6024  xpima  6041  xpexgALT  7684  curry1  7801  fparlem3  7811  fparlem4  7812  xp1en  8605  djuunxp  9352  dju1dif  9600  djuassen  9606  xpdjuen  9607  infdju1  9617  yonedalem3b  17531  yonedalem3  17532  pws1  19368  pwsmgp  19370  xkoinjcn  22297  imasdsf1olem  22985  df0op2  29531  ho01i  29607  nmop0h  29770  mbfmcst  31519  0rrv  31711  cvmlift2lem12  32563  zrdivrng  35233