Theorem xpeq1i 5667

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

Syntax hints:   = wceq 1540   × cxp 5639

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-opab 5173  df-xp 5647

This theorem is referenced by:  iunxpconst  5714  xpindi  5800  difxp2  6142  resdmres  6208  xpprsng  7115  curry2  8089  mapsnconst  8868  mapsncnv  8869  xp2dju  10137  pwdju1  10151  pwdjundom  10627  geomulcvg  15849  hofcl  18227  evlsval  22000  matvsca2  22322  ehl0  25324  ovoliunnul  25415  vitalilem5  25520  lgam1  26981  iunxpssiun1  32504  finxp2o  37394  finxp3o  37395  poimirlem3  37624  poimirlem5  37626  poimirlem10  37631  poimirlem22  37643  poimirlem23  37644  mendvscafval  43182  binomcxplemnn0  44345  itscnhlinecirc02plem3  48777  inlinecirc02p  48780