Theorem xpeq1i 5677

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

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

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-opab 5168  df-xp 5657

This theorem is used by:  iunxpconst  5724  xpindi  5810  difxp2  6157  resdmres  6232  xpprsng  7140  curry2  8116  mapsnconst  8913  mapsncnv  8914  xp2dju  10248  pwdju1  10262  pwdjundom  10745  indconst0  12325  indconst1  12326  geomulcvg  16038  hofcl  18426  evlsval  22388  matvsca2  22736  ehl0  25731  ovoliunnul  25821  vitalilem5  25926  lgam1  27384  iunxpssiun1  33155  1enumen  35712  finxp2o  38302  finxp3o  38303  poimirlem3  38521  poimirlem5  38523  poimirlem10  38528  poimirlem22  38540  poimirlem23  38541  mendvscafval  44172  binomcxplemnn0  45318  itscnhlinecirc02plem3  49865  inlinecirc02p  49868