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

Theorem xpeq2i 5707
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 5701 . 2 (𝐴 = 𝐵 → (𝐶 × 𝐴) = (𝐶 × 𝐵))
31, 2ax-mp 5 1 (𝐶 × 𝐴) = (𝐶 × 𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1533   × cxp 5678
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2698
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-sb 2060  df-clab 2705  df-cleq 2719  df-clel 2805  df-opab 5213  df-xp 5686
This theorem is referenced by:  xpindir  5839  xpssres  6025  difxp1  6172  xpima  6189  xpexgALT  7989  curry1  8113  fparlem3  8123  fparlem4  8124  xp1en  9086  djuunxp  9950  dju1dif  10201  djuassen  10207  xpdjuen  10208  infdju1  10218  yonedalem3b  18276  yonedalem3  18277  pws1  20266  pwsmgp  20268  xkoinjcn  23609  imasdsf1olem  24297  df0op2  31580  ho01i  31656  nmop0h  31819  mbfmcst  33884  0rrv  34076  cvmlift2lem12  34929  zrdivrng  37431
  Copyright terms: Public domain W3C validator