Theorem xpeq1i 5545

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

Syntax hints:   = wceq 1538   × cxp 5517

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-opab 5093  df-xp 5525

This theorem is referenced by:  iunxpconst  5588  xpindi  5668  difxp2  5990  resdmres  6056  xpprsng  6879  curry2  7785  mapsnconst  8439  mapsncnv  8440  xp2dju  9587  pwdju1  9601  pwdjundom  10078  geomulcvg  15224  hofcl  17501  evlsval  20758  matvsca2  21033  ehl0  24021  ovoliunnul  24111  vitalilem5  24216  lgam1  25649  finxp2o  34816  finxp3o  34817  poimirlem3  35060  poimirlem5  35062  poimirlem10  35067  poimirlem22  35079  poimirlem23  35080  mendvscafval  40134  binomcxplemnn0  41053  itscnhlinecirc02plem3  45198  inlinecirc02p  45201