Theorem xpeq1i 5685

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

Syntax hints:   = wceq 1567   × cxp 5657

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-opab 5175  df-xp 5665

This theorem is referenced by:  iunxpconst  5732  xpindi  5817  difxp2  6162  resdmres  6230  xpprsng  7134  curry2  8098  mapsnconst  8886  mapsncnv  8887  xp2dju  10156  pwdju1  10170  pwdjundom  10648  indconst0  12226  indconst1  12227  geomulcvg  15926  hofcl  18311  evlsval  22202  matvsca2  22550  ehl0  25541  ovoliunnul  25631  vitalilem5  25736  lgam1  27190  iunxpssiun1  32850  1enumen  35424  finxp2o  37928  finxp3o  37929  poimirlem3  38157  poimirlem5  38159  poimirlem10  38164  poimirlem22  38176  poimirlem23  38177  mendvscafval  43798  binomcxplemnn0  44944  itscnhlinecirc02plem3  49442  inlinecirc02p  49445