Theorem xpeq1i 5686

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

This proof depends on syntax axioms:   = wceq 1569   × cxp 5658

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-opab 5173  df-xp 5666

This theorem is used by:  iunxpconst  5733  xpindi  5818  difxp2  6162  resdmres  6232  xpprsng  7136  curry2  8100  mapsnconst  8888  mapsncnv  8889  xp2dju  10167  pwdju1  10181  pwdjundom  10658  indconst0  12236  indconst1  12237  geomulcvg  15937  hofcl  18321  evlsval  22248  matvsca2  22596  ehl0  25587  ovoliunnul  25677  vitalilem5  25782  lgam1  27239  iunxpssiun1  32924  1enumen  35494  finxp2o  38073  finxp3o  38074  poimirlem3  38302  poimirlem5  38304  poimirlem10  38309  poimirlem22  38321  poimirlem23  38322  mendvscafval  43941  binomcxplemnn0  45087  itscnhlinecirc02plem3  49592  inlinecirc02p  49595