MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xpeq1i Structured version   Visualization version   GIF version

Theorem xpeq1i 5615
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
StepHypRef Expression
1 xpeq1i.1 . 2 𝐴 = 𝐵
2 xpeq1 5603 . 2 (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶))
31, 2ax-mp 5 1 (𝐴 × 𝐶) = (𝐵 × 𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1539   × cxp 5587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-opab 5137  df-xp 5595
This theorem is referenced by:  iunxpconst  5659  xpindi  5742  difxp2  6069  resdmres  6135  xpprsng  7012  curry2  7947  mapsnconst  8680  mapsncnv  8681  xp2dju  9932  pwdju1  9946  pwdjundom  10423  geomulcvg  15588  hofcl  17977  evlsval  21296  matvsca2  21577  ehl0  24581  ovoliunnul  24671  vitalilem5  24776  lgam1  26213  finxp2o  35570  finxp3o  35571  poimirlem3  35780  poimirlem5  35782  poimirlem10  35787  poimirlem22  35799  poimirlem23  35800  mendvscafval  41015  binomcxplemnn0  41967  itscnhlinecirc02plem3  46130  inlinecirc02p  46133
  Copyright terms: Public domain W3C validator