Theorem xpeq1i 5059

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

Syntax hints:   = wceq 1475   × cxp 5036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-opab 4644  df-xp 5044

This theorem is referenced by:  iunxpconst  5098  xpindi  5177  difxp2  5479  resdmres  5543  curry2  7159  mapsnconst  7789  mapsncnv  7790  cda1dif  8881  cdaassen  8887  infcda1  8898  geomulcvg  14446  hofcl  16722  evlsval  19340  matvsca2  20053  ovoliunnul  23082  vitalilem5  23187  lgam1  24590  finxp2o  32412  finxp3o  32413  poimirlem3  32582  poimirlem5  32584  poimirlem10  32589  poimirlem22  32601  poimirlem23  32602  mendvscafval  36779  binomcxplemnn0  37570  xpprsng  41903