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

Theorem xpeq2i 4870
Description: Equality inference for Cartesian product. (Contributed by NM, 21-Dec-2008.)
Hypothesis
Ref Expression
xpeq1i.1  |-  A  =  B
Assertion
Ref Expression
xpeq2i  |-  ( C  X.  A )  =  ( C  X.  B
)

Proof of Theorem xpeq2i
StepHypRef Expression
1 xpeq1i.1 . 2  |-  A  =  B
2 xpeq2 4864 . 2  |-  ( A  =  B  ->  ( C  X.  A )  =  ( C  X.  B
) )
31, 2ax-mp 5 1  |-  ( C  X.  A )  =  ( C  X.  B
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    X. cxp 4847
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-opab 4480  df-xp 4855
This theorem is referenced by:  xpindir  4984  difxp1  5277  xpima  5294  xpexgALT  6796  curry1  6895  fparlem3  6905  fparlem4  6906  xp1en  7660  xp2cda  8610  xpcdaen  8613  pwcda1  8624  pwcdandom  9092  yonedalem3b  16149  yonedalem3  16150  pws1  17829  pwsmgp  17831  xkoinjcn  20686  imasdsf1olem  21372  zrdivrng  26143  df0op2  27388  ho01i  27464  nmop0h  27627  mbfmcst  29074  0rrv  29277  cvmlift2lem12  30030  xpheOLD  36232
  Copyright terms: Public domain W3C validator