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

Theorem rexeqdv 3061
Description: Equality deduction for restricted existential quantifier. (Contributed by NM, 14-Jan-2007.)
Hypothesis
Ref Expression
raleq1d.1
Assertion
Ref Expression
rexeqdv
Distinct variable groups:   ,   ,

Proof of Theorem rexeqdv
StepHypRef Expression
1 raleq1d.1 . 2
2 rexeq 3055 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  E.wrex 2808
This theorem is referenced by:  rexeqbidv  3069  rexeqbidva  3071  fnunirn  6165  oarec  7230  fival  7892  marypha1lem  7913  marypha1  7914  wemapwe  8160  wemapweOLD  8161  zornn0g  8906  scshwfzeqfzo  12794  supcvg  13667  zprod  13744  vdwlem6  14504  rami  14533  cshws0  14586  imasleval  14938  isssc  15189  ipodrsfi  15793  grppropd  16068  sylow1lem2  16619  sylow3lem1  16647  lsmass  16688  pj1fval  16712  efgrelexlema  16767  ablfacrplem  17116  pgpfac1lem2  17126  pgpfac1lem3  17128  pgpfac1lem4  17129  ablfac2  17140  dvdsrval  17294  dvdsrpropd  17345  znunit  18602  ellspd  18836  ellspdOLD  18837  cnpfval  19735  cmpcov  19889  cmpsublem  19899  cmpsub  19900  tgcmp  19901  uncmp  19903  hauscmplem  19906  bwthOLD  19911  1stcfb  19946  2ndcctbss  19956  1stcelcls  19962  llyi  19975  nllyi  19976  cldllycmp  19996  ptrescn  20140  isufl  20414  fmid  20461  alexsublem  20544  alexsubb  20546  alexsubALTlem4  20550  alexsubALT  20551  cnextfres  20568  tsmsf1o  20647  utopval  20735  imasf1oxms  20992  bndth  21458  ovolicc2  21933  ellimc2  22281  limcflf  22285  plyval  22590  aannenlem1  22724  aannenlem2  22725  ulm2  22780  ishpg  24128  nb3graprlem2  24452  fargshiftfo  24638  wwlkextsur  24731  erclwwlknsym  24826  erclwwlkntr  24827  hashecclwwlkn1  24834  usghashecclwwlk  24835  frgra2v  24999  isplig  25179  isgrp2d  25237  isgrpda  25299  pjhth  26311  pjhfval  26314  pjhtheu2  26334  iscref  27847  crefeq  27848  eulerpartlemgh  28317  ballotlemfc0  28431  ballotlemfcc  28432  ispcon  28668  br8  29185  br6  29186  br4  29187  wsuclem  29381  brsegle  29758  hilbert1.1  29804  limsucncmpi  29910  volsupnfl  30059  isdrngo2  30361  isnacs  30636  eldioph  30691  islssfg  31016  itgoval  31110  stoweidlem50  31832  stoweidlem57  31839  fullestrcsetc  32657  fullsetcestrc  32672  lco0  33028  lcvfbr  34745  lkrlspeqN  34896  pointsetN  35465  dia1dim2  36789  dib1dim2  36895  diclspsn  36921  dih1dimatlem  37056  lcfrvalsnN  37268  mapdpglem3  37402  mapdpglem26  37425  mapdpglem27  37426
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-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813
  Copyright terms: Public domain W3C validator