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

Theorem reurex 3052
 Description: Restricted unique existence implies restricted existence. (Contributed by NM, 19-Aug-1999.)
Assertion
Ref Expression
reurex

Proof of Theorem reurex
StepHypRef Expression
1 reu5 3051 . 2
21simplbi 461 1
 Colors of variables: wff setvar class Syntax hints:   wi 4  wrex 2783  wreu 2784  wrmo 2785 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 1751  ax-6 1797 This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-eu 2270  df-mo 2271  df-rex 2788  df-reu 2789  df-rmo 2790 This theorem is referenced by:  reu3  3267  sbcreu  3382  reuxfrd  4647  tz6.26  5430  weniso  6260  oawordex  7266  oaabs  7353  oaabs2  7354  supval2  7975  fisup2g  7990  nqerf  9354  qbtwnre  11492  modprm0  14719  meet0  16334  join0  16335  issrgid  17691  isringid  17741  lspsneu  18281  frgpcyg  19075  qtophmeo  20763  pjthlem2  22273  dyadmax  22433  quotlem  23121  frgra2v  25572  2pthfrgrarn  25582  frgrancvvdeqlemC  25612  frg2wotn0  25629  pjhthlem2  26880  cnlnadj  27567  reuxfr4d  27961  rmoxfrdOLD  27963  rmoxfrd  27964  cvmliftpht  29829  lcfl7N  34781  2reu2rex  38007  2rexreu  38009  2reu4  38014  isringrng  38651  uzlidlring  38699
 Copyright terms: Public domain W3C validator