Theorem xpeq1i 5669

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

Syntax hints:   = wceq 1559   × cxp 5641

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-opab 5160  df-xp 5649

This theorem is referenced by:  iunxpconst  5716  xpindi  5801  difxp2  6147  resdmres  6214  xpprsng  7117  curry2  8080  mapsnconst  8868  mapsncnv  8869  xp2dju  10127  pwdju1  10141  pwdjundom  10619  indconst0  12201  indconst1  12202  geomulcvg  15897  hofcl  18282  evlsval  22127  matvsca2  22476  ehl0  25467  ovoliunnul  25557  vitalilem5  25662  lgam1  27116  iunxpssiun1  32728  finxp2o  37854  finxp3o  37855  poimirlem3  38083  poimirlem5  38085  poimirlem10  38090  poimirlem22  38102  poimirlem23  38103  mendvscafval  43724  binomcxplemnn0  44886  itscnhlinecirc02plem3  49367  inlinecirc02p  49370