Theorem xpeq1i 5684

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-opab 5174  df-xp 5664

This theorem is used by:  iunxpconst  5731  xpindi  5820  difxp2  6175  resdmres  6252  xpprsng  7174  curry2  8155  mapsnconst  8958  mapsncnv  8959  xp2dju  10294  pwdju1  10308  pwdjundom  10791  indconst0  12372  indconst1  12373  geomulcvg  16089  hofcl  18483  evlsval  22450  matvsca2  22798  ehl0  25793  ovoliunnul  25883  vitalilem5  25988  lgam1  27448  iunxpssiun1  33260  1enumen  35848  finxp2o  38590  finxp3o  38591  poimirlem3  38809  poimirlem5  38811  poimirlem10  38816  poimirlem22  38828  poimirlem23  38829  mendvscafval  44449  binomcxplemnn0  45594  ehl2eudisval0  50169