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

Theorem xpeq2i 5007
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 5001 . 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 1381    X. cxp 4984
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-opab 4493  df-xp 4992
This theorem is referenced by:  xpindir  5124  difxp1  5419  xpima  5436  xpexgALT  6775  curry1  6874  fparlem3  6884  fparlem4  6885  xp1en  7602  xp2cda  8560  xpcdaen  8563  pwcda1  8574  pwcdandom  9045  yonedalem3b  15419  yonedalem3  15420  pws1  17136  pwsmgp  17138  xkoinjcn  20058  imasdsf1olem  20746  zrdivrng  25303  df0op2  26540  ho01i  26616  nmop0h  26779  mbfmcst  28100  0rrv  28260  cvmlift2lem12  28629  xphe  37474
  Copyright terms: Public domain W3C validator