Theorem xpeq1i 5615

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

Syntax hints:   = wceq 1539   × cxp 5587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-opab 5137  df-xp 5595

This theorem is referenced by:  iunxpconst  5659  xpindi  5742  difxp2  6069  resdmres  6135  xpprsng  7012  curry2  7947  mapsnconst  8680  mapsncnv  8681  xp2dju  9932  pwdju1  9946  pwdjundom  10423  geomulcvg  15588  hofcl  17977  evlsval  21296  matvsca2  21577  ehl0  24581  ovoliunnul  24671  vitalilem5  24776  lgam1  26213  finxp2o  35570  finxp3o  35571  poimirlem3  35780  poimirlem5  35782  poimirlem10  35787  poimirlem22  35799  poimirlem23  35800  mendvscafval  41015  binomcxplemnn0  41967  itscnhlinecirc02plem3  46130  inlinecirc02p  46133