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

Theorem xpeq2i 5373
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 5367 . 2 (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵))
31, 2ax-mp 5 1 (𝐶 × 𝐴) = (𝐶 × 𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1656   × cxp 5344
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-opab 4938  df-xp 5352
This theorem is referenced by:  xpindir  5493  xpssres  5673  difxp1  5804  xpima  5821  xpexgALT  7426  curry1  7538  fparlem3  7548  fparlem4  7549  xp1en  8321  djuunxp  9067  xp2cda  9324  xpcdaen  9327  pwcda1  9338  pwcdandom  9811  yonedalem3b  17279  yonedalem3  17280  pws1  18977  pwsmgp  18979  xkoinjcn  21868  imasdsf1olem  22555  df0op2  29162  ho01i  29238  nmop0h  29401  mbfmcst  30862  0rrv  31055  cvmlift2lem12  31838  zrdivrng  34293
  Copyright terms: Public domain W3C validator