Theorem xpeq1i 5685

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

Syntax hints:   = wceq 1540   × cxp 5657

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-opab 5187  df-xp 5665

This theorem is referenced by:  iunxpconst  5732  xpindi  5818  difxp2  6160  resdmres  6226  xpprsng  7135  curry2  8111  mapsnconst  8911  mapsncnv  8912  xp2dju  10196  pwdju1  10210  pwdjundom  10686  geomulcvg  15897  hofcl  18276  evlsval  22049  matvsca2  22371  ehl0  25374  ovoliunnul  25465  vitalilem5  25570  lgam1  27031  iunxpssiun1  32554  finxp2o  37422  finxp3o  37423  poimirlem3  37652  poimirlem5  37654  poimirlem10  37659  poimirlem22  37671  poimirlem23  37672  mendvscafval  43177  binomcxplemnn0  44340  itscnhlinecirc02plem3  48731  inlinecirc02p  48734