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

Theorem reu4 3293
Description: Restricted uniqueness using implicit substitution. (Contributed by NM, 23-Nov-1994.)
Hypothesis
Ref Expression
rmo4.1
Assertion
Ref Expression
reu4
Distinct variable groups:   , ,   ,   ,

Proof of Theorem reu4
StepHypRef Expression
1 reu5 3073 . 2
2 rmo4.1 . . . 4
32rmo4 3292 . . 3
43anbi2i 694 . 2
51, 4bitri 249 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  A.wral 2807  E.wrex 2808  E!wreu 2809  E*wrmo 2810
This theorem is referenced by:  reuind  3303  oawordeulem  7222  fin23lem23  8727  nqereu  9328  receu  10219  lbreu  10518  cju  10557  fprodser  13756  divalglem9  14059  ndvdssub  14065  qredeu  14248  pj1eu  16714  efgredeu  16770  lspsneu  17769  qtopeu  20217  qtophmeo  20318  minveclem7  21850  ig1peu  22572  coeeu  22622  plydivalg  22695  mirreu3  24035  axcontlem2  24268  usgra2edg1  24383  usgraedgreu  24388  nbgraf1olem1  24441  4cycl2vnunb  25017  frg2wot1  25057  exidu1  25328  rngoideu  25386  minvecolem7  25799  hlimreui  26157  riesz4i  26982  cdjreui  27351  xreceu  27618  cvmseu  28721  nocvxmin  29451  segconeu  29661  outsideofeu  29781  bfp  30320  mpaaeu  31099  usgvincvadeu  32405  usgvincvadeuALT  32408  usg2edgneu  32412  lshpsmreu  34834  cdleme  36286  lcfl7N  37228  mapdpg  37433  hdmap14lem6  37603
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-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-cleq 2449  df-clel 2452  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815
  Copyright terms: Public domain W3C validator