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

Theorem xpeq1i 5552
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 5540 . 2 (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶))
31, 2ax-mp 5 1 (𝐴 × 𝐶) = (𝐵 × 𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542   × cxp 5524
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 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-opab 5094  df-xp 5532
This theorem is referenced by:  iunxpconst  5596  xpindi  5677  difxp2  5999  resdmres  6065  xpprsng  6915  curry2  7831  mapsnconst  8505  mapsncnv  8506  xp2dju  9679  pwdju1  9693  pwdjundom  10170  geomulcvg  15327  hofcl  17628  evlsval  20903  matvsca2  21182  ehl0  24172  ovoliunnul  24262  vitalilem5  24367  lgam1  25804  finxp2o  35216  finxp3o  35217  poimirlem3  35426  poimirlem5  35428  poimirlem10  35433  poimirlem22  35445  poimirlem23  35446  mendvscafval  40610  binomcxplemnn0  41528  itscnhlinecirc02plem3  45694  inlinecirc02p  45697
  Copyright terms: Public domain W3C validator