Theorem xpeq1i 5606

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

Syntax hints:   = wceq 1539   × cxp 5578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-opab 5133  df-xp 5586

This theorem is referenced by:  iunxpconst  5650  xpindi  5731  difxp2  6058  resdmres  6124  xpprsng  6994  curry2  7918  mapsnconst  8638  mapsncnv  8639  xp2dju  9863  pwdju1  9877  pwdjundom  10354  geomulcvg  15516  hofcl  17893  evlsval  21206  matvsca2  21485  ehl0  24486  ovoliunnul  24576  vitalilem5  24681  lgam1  26118  finxp2o  35497  finxp3o  35498  poimirlem3  35707  poimirlem5  35709  poimirlem10  35714  poimirlem22  35726  poimirlem23  35727  mendvscafval  40931  binomcxplemnn0  41856  itscnhlinecirc02plem3  46018  inlinecirc02p  46021