Theorem xpeq1i 5715

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

Syntax hints:   = wceq 1537   × cxp 5687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-opab 5211  df-xp 5695

This theorem is referenced by:  iunxpconst  5761  xpindi  5847  difxp2  6188  resdmres  6254  xpprsng  7160  curry2  8131  mapsnconst  8931  mapsncnv  8932  xp2dju  10215  pwdju1  10229  pwdjundom  10705  geomulcvg  15909  hofcl  18316  evlsval  22128  matvsca2  22450  ehl0  25465  ovoliunnul  25556  vitalilem5  25661  lgam1  27122  finxp2o  37382  finxp3o  37383  poimirlem3  37610  poimirlem5  37612  poimirlem10  37617  poimirlem22  37629  poimirlem23  37630  mendvscafval  43175  binomcxplemnn0  44345  itscnhlinecirc02plem3  48634  inlinecirc02p  48637