Theorem xpeq1i 5657

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

Syntax hints:   = wceq 1542   × cxp 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-opab 5148  df-xp 5637

This theorem is referenced by:  iunxpconst  5704  xpindi  5788  difxp2  6130  resdmres  6196  xpprsng  7093  curry2  8057  mapsnconst  8840  mapsncnv  8841  xp2dju  10099  pwdju1  10113  pwdjundom  10590  indconst0  12171  indconst1  12172  geomulcvg  15841  hofcl  18225  evlsval  22064  matvsca2  22393  ehl0  25384  ovoliunnul  25474  vitalilem5  25579  lgam1  27027  iunxpssiun1  32638  finxp2o  37715  finxp3o  37716  poimirlem3  37944  poimirlem5  37946  poimirlem10  37951  poimirlem22  37963  poimirlem23  37964  mendvscafval  43614  binomcxplemnn0  44776  itscnhlinecirc02plem3  49260  inlinecirc02p  49263