Theorem xpeq1i 5681

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

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

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-opab 5168  df-xp 5661

This theorem is used by:  iunxpconst  5728  xpindi  5813  difxp2  6158  resdmres  6228  xpprsng  7135  curry2  8104  mapsnconst  8899  mapsncnv  8900  xp2dju  10179  pwdju1  10193  pwdjundom  10676  indconst0  12254  indconst1  12255  geomulcvg  15965  hofcl  18347  evlsval  22302  matvsca2  22650  ehl0  25645  ovoliunnul  25735  vitalilem5  25840  lgam1  27300  iunxpssiun1  33041  1enumen  35599  finxp2o  38153  finxp3o  38154  poimirlem3  38372  poimirlem5  38374  poimirlem10  38379  poimirlem22  38391  poimirlem23  38392  mendvscafval  44027  binomcxplemnn0  45173  itscnhlinecirc02plem3  49714  inlinecirc02p  49717