Theorem xpeq2i 5373

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

Syntax hints:   = wceq 1656   × cxp 5344

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-opab 4938  df-xp 5352

This theorem is referenced by:  xpindir  5493  xpssres  5673  difxp1  5804  xpima  5821  xpexgALT  7426  curry1  7538  fparlem3  7548  fparlem4  7549  xp1en  8321  djuunxp  9067  xp2cda  9324  xpcdaen  9327  pwcda1  9338  pwcdandom  9811  yonedalem3b  17279  yonedalem3  17280  pws1  18977  pwsmgp  18979  xkoinjcn  21868  imasdsf1olem  22555  df0op2  29162  ho01i  29238  nmop0h  29401  mbfmcst  30862  0rrv  31055  cvmlift2lem12  31838  zrdivrng  34293