Theorem xpeq1i 5726

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

Syntax hints:   = wceq 1537   × cxp 5698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-opab 5229  df-xp 5706

This theorem is referenced by:  iunxpconst  5772  xpindi  5858  difxp2  6197  resdmres  6263  xpprsng  7174  curry2  8148  mapsnconst  8950  mapsncnv  8951  xp2dju  10246  pwdju1  10260  pwdjundom  10736  geomulcvg  15924  hofcl  18329  evlsval  22133  matvsca2  22455  ehl0  25470  ovoliunnul  25561  vitalilem5  25666  lgam1  27125  finxp2o  37365  finxp3o  37366  poimirlem3  37583  poimirlem5  37585  poimirlem10  37590  poimirlem22  37602  poimirlem23  37603  mendvscafval  43147  binomcxplemnn0  44318  itscnhlinecirc02plem3  48518  inlinecirc02p  48521