Theorem xpeq1i 5649

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

Syntax hints:   = wceq 1540   × cxp 5621

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 5158  df-xp 5629

This theorem is referenced by:  iunxpconst  5696  xpindi  5780  difxp2  6119  resdmres  6185  xpprsng  7078  curry2  8047  mapsnconst  8826  mapsncnv  8827  xp2dju  10090  pwdju1  10104  pwdjundom  10580  geomulcvg  15802  hofcl  18184  evlsval  22010  matvsca2  22332  ehl0  25334  ovoliunnul  25425  vitalilem5  25530  lgam1  26991  iunxpssiun1  32531  finxp2o  37392  finxp3o  37393  poimirlem3  37622  poimirlem5  37624  poimirlem10  37629  poimirlem22  37641  poimirlem23  37642  mendvscafval  43179  binomcxplemnn0  44342  itscnhlinecirc02plem3  48789  inlinecirc02p  48792