Theorem xpeq1i 5552

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

Syntax hints:   = wceq 1542   × cxp 5524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-opab 5094  df-xp 5532

This theorem is referenced by:  iunxpconst  5596  xpindi  5677  difxp2  5999  resdmres  6065  xpprsng  6915  curry2  7831  mapsnconst  8505  mapsncnv  8506  xp2dju  9679  pwdju1  9693  pwdjundom  10170  geomulcvg  15327  hofcl  17628  evlsval  20903  matvsca2  21182  ehl0  24172  ovoliunnul  24262  vitalilem5  24367  lgam1  25804  finxp2o  35216  finxp3o  35217  poimirlem3  35426  poimirlem5  35428  poimirlem10  35433  poimirlem22  35445  poimirlem23  35446  mendvscafval  40610  binomcxplemnn0  41528  itscnhlinecirc02plem3  45694  inlinecirc02p  45697