Theorem xpeq1i 5689

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

This proof depends on syntax axioms:   = wceq 1570   × cxp 5661

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-opab 5176  df-xp 5669

This theorem is used by:  iunxpconst  5736  xpindi  5821  difxp2  6165  resdmres  6235  xpprsng  7140  curry2  8104  mapsnconst  8892  mapsncnv  8893  xp2dju  10172  pwdju1  10186  pwdjundom  10663  indconst0  12241  indconst1  12242  geomulcvg  15948  hofcl  18332  evlsval  22266  matvsca2  22614  ehl0  25605  ovoliunnul  25695  vitalilem5  25800  lgam1  27257  iunxpssiun1  32942  1enumen  35502  finxp2o  38078  finxp3o  38079  poimirlem3  38307  poimirlem5  38309  poimirlem10  38314  poimirlem22  38326  poimirlem23  38327  mendvscafval  43946  binomcxplemnn0  45092  itscnhlinecirc02plem3  49597  inlinecirc02p  49600