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

Theorem xpeq2i 5553
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 5547 . 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 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-opab 5094  df-xp 5532
This theorem is referenced by:  xpindir  5678  xpssres  5863  difxp1  5998  xpima  6015  xpexgALT  7708  curry1  7826  fparlem3  7836  fparlem4  7837  xp1en  8653  djuunxp  9424  dju1dif  9673  djuassen  9679  xpdjuen  9680  infdju1  9690  yonedalem3b  17646  yonedalem3  17647  pws1  19489  pwsmgp  19491  xkoinjcn  22439  imasdsf1olem  23127  df0op2  29687  ho01i  29763  nmop0h  29926  mbfmcst  31796  0rrv  31988  cvmlift2lem12  32847  zrdivrng  35731
  Copyright terms: Public domain W3C validator