Theorem xpeq1i 5657

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

Syntax hints:   = wceq 1540   × cxp 5629

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 5165  df-xp 5637

This theorem is referenced by:  iunxpconst  5704  xpindi  5787  difxp2  6127  resdmres  6193  xpprsng  7094  curry2  8063  mapsnconst  8842  mapsncnv  8843  xp2dju  10106  pwdju1  10120  pwdjundom  10596  geomulcvg  15818  hofcl  18196  evlsval  21969  matvsca2  22291  ehl0  25293  ovoliunnul  25384  vitalilem5  25489  lgam1  26950  iunxpssiun1  32470  finxp2o  37360  finxp3o  37361  poimirlem3  37590  poimirlem5  37592  poimirlem10  37597  poimirlem22  37609  poimirlem23  37610  mendvscafval  43148  binomcxplemnn0  44311  itscnhlinecirc02plem3  48746  inlinecirc02p  48749