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

Theorem xpeq2i 5712
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 5706 . 2 (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵))
31, 2ax-mp 5 1 (𝐶 × 𝐴) = (𝐶 × 𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540   × cxp 5683
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-opab 5206  df-xp 5691
This theorem is referenced by:  xpindir  5845  xpssres  6036  difxp1  6185  xpima  6202  xpexgALT  8006  curry1  8129  fparlem3  8139  fparlem4  8140  xp1en  9097  djuunxp  9961  dju1dif  10213  djuassen  10219  xpdjuen  10220  infdju1  10230  yonedalem3b  18324  yonedalem3  18325  pws1  20322  pwsmgp  20324  xkoinjcn  23695  imasdsf1olem  24383  df0op2  31771  ho01i  31847  nmop0h  32010  mbfmcst  34261  0rrv  34453  cvmlift2lem12  35319  zrdivrng  37960
  Copyright terms: Public domain W3C validator