Theorem xpeq1i 5583

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

Syntax hints:   = wceq 1537   × cxp 5555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-opab 5131  df-xp 5563

This theorem is referenced by:  iunxpconst  5626  xpindi  5706  difxp2  6025  resdmres  6091  xpprsng  6904  curry2  7804  mapsnconst  8458  mapsncnv  8459  xp2dju  9604  pwdju1  9618  pwdjundom  10091  geomulcvg  15234  hofcl  17511  evlsval  20301  matvsca2  21039  ehl0  24022  ovoliunnul  24110  vitalilem5  24215  lgam1  25643  finxp2o  34682  finxp3o  34683  poimirlem3  34897  poimirlem5  34899  poimirlem10  34904  poimirlem22  34916  poimirlem23  34917  mendvscafval  39797  binomcxplemnn0  40688  itscnhlinecirc02plem3  44778  inlinecirc02p  44781