Theorem xpeq1i 5703

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

Syntax hints:   = wceq 1542   × cxp 5675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-opab 5212  df-xp 5683

This theorem is referenced by:  iunxpconst  5749  xpindi  5834  difxp2  6166  resdmres  6232  xpprsng  7138  curry2  8093  mapsnconst  8886  mapsncnv  8887  xp2dju  10171  pwdju1  10185  pwdjundom  10662  geomulcvg  15822  hofcl  18212  evlsval  21649  matvsca2  21930  ehl0  24934  ovoliunnul  25024  vitalilem5  25129  lgam1  26568  finxp2o  36280  finxp3o  36281  poimirlem3  36491  poimirlem5  36493  poimirlem10  36498  poimirlem22  36510  poimirlem23  36511  mendvscafval  41932  binomcxplemnn0  43108  itscnhlinecirc02plem3  47470  inlinecirc02p  47473