Theorem xpeq1i 5658

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

Syntax hints:   = wceq 1542   × cxp 5630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-opab 5163  df-xp 5638

This theorem is referenced by:  iunxpconst  5705  xpindi  5790  difxp2  6132  resdmres  6198  xpprsng  7095  curry2  8059  mapsnconst  8842  mapsncnv  8843  xp2dju  10099  pwdju1  10113  pwdjundom  10590  geomulcvg  15811  hofcl  18194  evlsval  22053  matvsca2  22384  ehl0  25385  ovoliunnul  25476  vitalilem5  25581  lgam1  27042  iunxpssiun1  32654  indconst0  32949  indconst1  32950  finxp2o  37651  finxp3o  37652  poimirlem3  37871  poimirlem5  37873  poimirlem10  37878  poimirlem22  37890  poimirlem23  37891  mendvscafval  43540  binomcxplemnn0  44702  itscnhlinecirc02plem3  49141  inlinecirc02p  49144