Theorem xpeq1i 5692

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

Syntax hints:   = wceq 1533   × cxp 5664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-opab 5201  df-xp 5672

This theorem is referenced by:  iunxpconst  5738  xpindi  5823  difxp2  6155  resdmres  6221  xpprsng  7130  curry2  8087  mapsnconst  8882  mapsncnv  8883  xp2dju  10167  pwdju1  10181  pwdjundom  10658  geomulcvg  15819  hofcl  18214  evlsval  21959  matvsca2  22252  ehl0  25267  ovoliunnul  25358  vitalilem5  25463  lgam1  26912  finxp2o  36770  finxp3o  36771  poimirlem3  36981  poimirlem5  36983  poimirlem10  36988  poimirlem22  37000  poimirlem23  37001  mendvscafval  42421  binomcxplemnn0  43597  itscnhlinecirc02plem3  47658  inlinecirc02p  47661