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

Theorem xpeq1i 5059
 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 5052 . 2 (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶))
31, 2ax-mp 5 1 (𝐴 × 𝐶) = (𝐵 × 𝐶)
 Colors of variables: wff setvar class Syntax hints:   = wceq 1475   × cxp 5036 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-opab 4644  df-xp 5044 This theorem is referenced by:  iunxpconst  5098  xpindi  5177  difxp2  5479  resdmres  5543  curry2  7159  mapsnconst  7789  mapsncnv  7790  cda1dif  8881  cdaassen  8887  infcda1  8898  geomulcvg  14446  hofcl  16722  evlsval  19340  matvsca2  20053  ovoliunnul  23082  vitalilem5  23187  lgam1  24590  finxp2o  32412  finxp3o  32413  poimirlem3  32582  poimirlem5  32584  poimirlem10  32589  poimirlem22  32601  poimirlem23  32602  mendvscafval  36779  binomcxplemnn0  37570  xpprsng  41903
 Copyright terms: Public domain W3C validator