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

Theorem xpeq2i 5558
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 5552 . 2 (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵))
31, 2ax-mp 5 1 (𝐶 × 𝐴) = (𝐶 × 𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1537   × cxp 5529
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-12 2177  ax-ext 2792
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-opab 5105  df-xp 5537
This theorem is referenced by:  xpindir  5681  xpssres  5865  difxp1  5998  xpima  6015  xpexgALT  7660  curry1  7777  fparlem3  7787  fparlem4  7788  xp1en  8581  djuunxp  9328  dju1dif  9576  djuassen  9582  xpdjuen  9583  infdju1  9593  yonedalem3b  17508  yonedalem3  17509  pws1  19345  pwsmgp  19347  xkoinjcn  22271  imasdsf1olem  22959  df0op2  29514  ho01i  29590  nmop0h  29753  mbfmcst  31525  0rrv  31717  cvmlift2lem12  32569  zrdivrng  35267
  Copyright terms: Public domain W3C validator