Theorem xpeq1i 5689

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

Syntax hints:   = wceq 1570   × cxp 5661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-opab 5175  df-xp 5669

This theorem is referenced by:  iunxpconst  5736  xpindi  5821  difxp2  6165  resdmres  6235  xpprsng  7138  curry2  8103  mapsnconst  8891  mapsncnv  8892  xp2dju  10161  pwdju1  10175  pwdjundom  10653  indconst0  12231  indconst1  12232  geomulcvg  15932  hofcl  18316  evlsval  22218  matvsca2  22566  ehl0  25557  ovoliunnul  25647  vitalilem5  25752  lgam1  27209  iunxpssiun1  32894  1enumen  35466  finxp2o  38026  finxp3o  38027  poimirlem3  38255  poimirlem5  38257  poimirlem10  38262  poimirlem22  38274  poimirlem23  38275  mendvscafval  43896  binomcxplemnn0  45042  itscnhlinecirc02plem3  49547  inlinecirc02p  49550