Theorem xpeq1i 5701

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

Syntax hints:   = wceq 1539   × cxp 5673

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-opab 5210  df-xp 5681

This theorem is referenced by:  iunxpconst  5747  xpindi  5832  difxp2  6164  resdmres  6230  xpprsng  7139  curry2  8095  mapsnconst  8888  mapsncnv  8889  xp2dju  10173  pwdju1  10187  pwdjundom  10664  geomulcvg  15826  hofcl  18216  evlsval  21868  matvsca2  22150  ehl0  25165  ovoliunnul  25256  vitalilem5  25361  lgam1  26804  finxp2o  36583  finxp3o  36584  poimirlem3  36794  poimirlem5  36796  poimirlem10  36801  poimirlem22  36813  poimirlem23  36814  mendvscafval  42234  binomcxplemnn0  43410  itscnhlinecirc02plem3  47557  inlinecirc02p  47560