Theorem xpeq1i 5676

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

This proof depends on syntax axioms:   = wceq 1569   × cxp 5648

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-opab 5167  df-xp 5656

This theorem is used by:  iunxpconst  5723  xpindi  5809  difxp2  6156  resdmres  6233  xpprsng  7143  curry2  8121  mapsnconst  8924  mapsncnv  8925  xp2dju  10259  pwdju1  10273  pwdjundom  10756  indconst0  12336  indconst1  12337  geomulcvg  16051  hofcl  18439  evlsval  22401  matvsca2  22749  ehl0  25744  ovoliunnul  25834  vitalilem5  25939  lgam1  27397  iunxpssiun1  33210  1enumen  35776  finxp2o  38416  finxp3o  38417  poimirlem3  38635  poimirlem5  38637  poimirlem10  38642  poimirlem22  38654  poimirlem23  38655  mendvscafval  44282  binomcxplemnn0  45427  ehl2eudisval0  49932  itscnhlinecirc02plem3  49990  inlinecirc02p  49993