Theorem xpeq1i 5135

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

Syntax hints:   = wceq 1483   × cxp 5112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-opab 4713  df-xp 5120

This theorem is referenced by:  iunxpconst  5175  xpindi  5255  difxp2  5560  resdmres  5625  curry2  7272  mapsnconst  7903  mapsncnv  7904  cda1dif  8998  cdaassen  9004  infcda1  9015  geomulcvg  14607  hofcl  16899  evlsval  19519  matvsca2  20234  ovoliunnul  23275  vitalilem5  23381  lgam1  24790  finxp2o  33236  finxp3o  33237  poimirlem3  33412  poimirlem5  33414  poimirlem10  33419  poimirlem22  33431  poimirlem23  33432  mendvscafval  37760  binomcxplemnn0  38548  xpprsng  42110