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

Theorem xpeq2d 5028
Description: Equality deduction for Cartesian product. (Contributed by Jeff Madsen, 17-Jun-2010.)
Hypothesis
Ref Expression
xpeq1d.1
Assertion
Ref Expression
xpeq2d

Proof of Theorem xpeq2d
StepHypRef Expression
1 xpeq1d.1 . 2
2 xpeq2 5019 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  X.cxp 5002
This theorem is referenced by:  xpriindi  5144  csbres  5281  csbresgOLD  5282  fconstg  5777  curry2  6895  fparlem4  6903  fvdiagfn  7483  mapsncnv  7485  xpsneng  7622  xpcdaen  8584  axdc4lem  8856  fpwwe2lem13  9041  expval  12168  imasvscafn  14934  comfffval  15093  fuchom  15330  homafval  15356  setcmon  15414  xpccofval  15451  pwsco2mhm  16002  frmdplusg  16022  mulgfval  16143  mulgval  16144  symgplusg  16414  efgval  16735  psrplusg  18034  psrvscafval  18043  psrvsca  18044  opsrle  18140  evlssca  18191  mpfind  18205  coe1fv  18245  coe1tm  18314  pf1ind  18391  pjfval  18737  frlmval  18779  islindf5  18874  mdetunilem4  19117  mdetunilem9  19122  txindislem  20134  txcmplem2  20143  txhaus  20148  txkgen  20153  xkofvcn  20185  xkoinjcn  20188  cnextval  20561  cnextfval  20562  pcorev2  21528  pcophtb  21529  pi1grplem  21549  pi1inv  21552  dvfval  22301  dvnfval  22325  0dgrb  22643  dgrnznn  22644  dgreq0  22662  dgrmulc  22668  plyrem  22701  facth  22702  fta1  22704  aaliou2  22736  taylfval  22754  taylpfval  22760  gxval  25260  0ofval  25702  indval2  28028  sxbrsigalem3  28243  sxbrsigalem2  28257  eulerpartlemgu  28316  sseqval  28327  sconpht  28674  sconpht2  28683  sconpi1  28684  cvmlift2lem11  28758  cvmlift2lem12  28759  cvmlift2lem13  28760  cvmlift3lem9  28772  mexval  28862  mexval2  28863  mdvval  28864  mpstval  28895  elima4  29209  ismrer1  30334  mzpclval  30657  mzpcl1  30661  mendvsca  31140  dvconstbi  31239  expgrowth  31240  bj-xtageq  34546  lflsc0N  34808  lkrscss  34823  lfl1dim  34846  lfl1dim2N  34847  ldualvs  34862
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-opab 4511  df-xp 5010
  Copyright terms: Public domain W3C validator