Theorem xpeq1i 5650

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

Syntax hints:   = wceq 1541   × cxp 5622

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 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-opab 5161  df-xp 5630

This theorem is referenced by:  iunxpconst  5697  xpindi  5782  difxp2  6124  resdmres  6190  xpprsng  7085  curry2  8049  mapsnconst  8830  mapsncnv  8831  xp2dju  10087  pwdju1  10101  pwdjundom  10578  geomulcvg  15799  hofcl  18182  evlsval  22041  matvsca2  22372  ehl0  25373  ovoliunnul  25464  vitalilem5  25569  lgam1  27030  iunxpssiun1  32643  indconst0  32939  indconst1  32940  finxp2o  37604  finxp3o  37605  poimirlem3  37824  poimirlem5  37826  poimirlem10  37831  poimirlem22  37843  poimirlem23  37844  mendvscafval  43428  binomcxplemnn0  44590  itscnhlinecirc02plem3  49030  inlinecirc02p  49033