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

Theorem xpeq2i 5616
Description: Equality inference for Cartesian product. (Contributed by NM, 21-Dec-2008.)
Hypothesis
Ref Expression
xpeq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
xpeq2i (𝐶 × 𝐴) = (𝐶 × 𝐵)

Proof of Theorem xpeq2i
StepHypRef Expression
1 xpeq1i.1 . 2 𝐴 = 𝐵
2 xpeq2 5610 . 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:  xpindir  5743  xpssres  5928  difxp1  6068  xpima  6085  xpexgALT  7824  curry1  7944  fparlem3  7954  fparlem4  7955  xp1en  8844  djuunxp  9679  dju1dif  9928  djuassen  9934  xpdjuen  9935  infdju1  9945  yonedalem3b  17997  yonedalem3  17998  pws1  19855  pwsmgp  19857  xkoinjcn  22838  imasdsf1olem  23526  df0op2  30114  ho01i  30190  nmop0h  30353  mbfmcst  32226  0rrv  32418  cvmlift2lem12  33276  zrdivrng  36111
  Copyright terms: Public domain W3C validator