Theorem xpeq1i 5644

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

Syntax hints:   = wceq 1547   × cxp 5616

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-opab 5135  df-xp 5624

This theorem is referenced by:  iunxpconst  5691  xpindi  5775  difxp2  6117  resdmres  6183  xpprsng  7082  curry2  8046  mapsnconst  8830  mapsncnv  8831  xp2dju  10090  pwdju1  10104  pwdjundom  10581  indconst0  12162  indconst1  12163  geomulcvg  15832  hofcl  18216  evlsval  22062  matvsca2  22411  ehl0  25402  ovoliunnul  25492  vitalilem5  25597  lgam1  27045  iunxpssiun1  32657  finxp2o  37761  finxp3o  37762  poimirlem3  37990  poimirlem5  37992  poimirlem10  37997  poimirlem22  38009  poimirlem23  38010  mendvscafval  43631  binomcxplemnn0  44793  itscnhlinecirc02plem3  49275  inlinecirc02p  49278