Theorem xpeq1i 5637

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

Syntax hints:   = wceq 1541   × cxp 5609

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-opab 5149  df-xp 5617

This theorem is referenced by:  iunxpconst  5684  xpindi  5768  difxp2  6108  resdmres  6174  xpprsng  7068  curry2  8032  mapsnconst  8811  mapsncnv  8812  xp2dju  10063  pwdju1  10077  pwdjundom  10553  geomulcvg  15778  hofcl  18160  evlsval  22016  matvsca2  22338  ehl0  25339  ovoliunnul  25430  vitalilem5  25535  lgam1  26996  iunxpssiun1  32540  finxp2o  37433  finxp3o  37434  poimirlem3  37663  poimirlem5  37665  poimirlem10  37670  poimirlem22  37682  poimirlem23  37683  mendvscafval  43219  binomcxplemnn0  44382  itscnhlinecirc02plem3  48816  inlinecirc02p  48819