Theorem xpeq1i 5650

Description: Equality inference for Cartesian product. (Contributed by NM, 21-Dec-2008.)

Hypothesis

Ref	Expression
xpeq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
xpeq1i	⊢ (𝐴 × 𝐶) = (𝐵 × 𝐶)

Proof of Theorem xpeq1i

Step	Hyp	Ref	Expression
1		xpeq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		xpeq1 5638	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 × 𝐶) = (𝐵 × 𝐶)

Syntax hints:   = wceq 1542   × cxp 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-opab 5149  df-xp 5630

This theorem is referenced by:  iunxpconst  5697  xpindi  5782  difxp2  6124  resdmres  6190  xpprsng  7087  curry2  8050  mapsnconst  8833  mapsncnv  8834  xp2dju  10090  pwdju1  10104  pwdjundom  10581  indconst0  12162  indconst1  12163  geomulcvg  15832  hofcl  18216  evlsval  22074  matvsca2  22403  ehl0  25394  ovoliunnul  25484  vitalilem5  25589  lgam1  27041  iunxpssiun1  32653  finxp2o  37729  finxp3o  37730  poimirlem3  37958  poimirlem5  37960  poimirlem10  37965  poimirlem22  37977  poimirlem23  37978  mendvscafval  43632  binomcxplemnn0  44794  itscnhlinecirc02plem3  49272  inlinecirc02p  49275