Theorem xpeq1i 5647

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

Syntax hints:   = wceq 1541   × cxp 5619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-opab 5158  df-xp 5627

This theorem is referenced by:  iunxpconst  5694  xpindi  5779  difxp2  6121  resdmres  6187  xpprsng  7082  curry2  8046  mapsnconst  8826  mapsncnv  8827  xp2dju  10079  pwdju1  10093  pwdjundom  10569  geomulcvg  15790  hofcl  18173  evlsval  22032  matvsca2  22363  ehl0  25364  ovoliunnul  25455  vitalilem5  25560  lgam1  27021  iunxpssiun1  32569  indconst0  32867  indconst1  32868  finxp2o  37516  finxp3o  37517  poimirlem3  37736  poimirlem5  37738  poimirlem10  37743  poimirlem22  37755  poimirlem23  37756  mendvscafval  43343  binomcxplemnn0  44506  itscnhlinecirc02plem3  48946  inlinecirc02p  48949