Theorem xpeq1i 5664

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

Syntax hints:   = wceq 1540   × cxp 5636

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-opab 5170  df-xp 5644

This theorem is referenced by:  iunxpconst  5711  xpindi  5797  difxp2  6139  resdmres  6205  xpprsng  7112  curry2  8086  mapsnconst  8865  mapsncnv  8866  xp2dju  10130  pwdju1  10144  pwdjundom  10620  geomulcvg  15842  hofcl  18220  evlsval  21993  matvsca2  22315  ehl0  25317  ovoliunnul  25408  vitalilem5  25513  lgam1  26974  iunxpssiun1  32497  finxp2o  37387  finxp3o  37388  poimirlem3  37617  poimirlem5  37619  poimirlem10  37624  poimirlem22  37636  poimirlem23  37637  mendvscafval  43175  binomcxplemnn0  44338  itscnhlinecirc02plem3  48773  inlinecirc02p  48776