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

Theorem reu5 3051
 Description: Restricted uniqueness in terms of "at most one." (Contributed by NM, 23-May-1999.) (Revised by NM, 16-Jun-2017.)
Assertion
Ref Expression
reu5

Proof of Theorem reu5
StepHypRef Expression
1 eu5 2294 . 2
2 df-reu 2789 . 2
3 df-rex 2788 . . 3
4 df-rmo 2790 . . 3
53, 4anbi12i 701 . 2
61, 2, 53bitr4i 280 1
 Colors of variables: wff setvar class Syntax hints:   wb 187   wa 370  wex 1659   wcel 1870  weu 2266  wmo 2267  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:  reurex  3052  reurmo  3053  reu4  3271  reueq  3275  reusv1  4625  wereu  4850  wereu2  4851  fncnv  5665  moriotass  6295  supeu  7974  resqreu  13295  sqrtneg  13310  sqreu  13402  catideu  15532  poslubd  16345  ismgmid  16458  mndideu  16501  evlseu  18674  frlmup4  19290  ply1divalg  22963  tglinethrueu  24543  foot  24621  mideu  24637  pjhtheu  26882  pjpreeq  26886  cnlnadjeui  27565  cvmliftlem14  29808  cvmlift2lem13  29826  cvmlift3  29839  linethrueu  30708  phpreu  31636  poimirlem18  31665  poimirlem21  31668  2reu5a  38001  reuan  38004  2reurex  38005  2rexreu  38009  2reu1  38010
 Copyright terms: Public domain W3C validator