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

Theorem reu5 3307
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 df-eu 2582 . 2 (∃!𝑥(𝑥𝐴𝜑) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ ∃*𝑥(𝑥𝐴𝜑)))
2 df-reu 3062 . 2 (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))
3 df-rex 3061 . . 3 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
4 df-rmo 3063 . . 3 (∃*𝑥𝐴 𝜑 ↔ ∃*𝑥(𝑥𝐴𝜑))
53, 4anbi12i 620 . 2 ((∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ ∃*𝑥(𝑥𝐴𝜑)))
61, 2, 53bitr4i 294 1 (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384  wex 1874  wcel 2155  ∃*wmo 2563  ∃!weu 2581  wrex 3056  ∃!wreu 3057  ∃*wrmo 3058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 198  df-an 385  df-eu 2582  df-rex 3061  df-reu 3062  df-rmo 3063
This theorem is referenced by:  reurex  3308  reurmo  3309  reu4  3559  reueq  3565  reusv1  5032  wereu  5273  wereu2  5274  fncnv  6140  moriotass  6832  supeu  8567  infeu  8609  resqreu  14280  sqrtneg  14295  sqreu  14387  catideu  16603  poslubd  17416  ismgmid  17532  mndideu  17572  evlseu  19789  frlmup4  20416  ply1divalg  24188  tglinethrueu  25825  foot  25905  mideu  25921  nbusgredgeu  26546  pjhtheu  28644  pjpreeq  28648  cnlnadjeui  29327  cvmliftlem14  31659  cvmlift2lem13  31677  cvmlift3  31690  nosupno  32225  nosupbday  32227  nosupbnd1  32236  nosupbnd2  32238  linethrueu  32639  phpreu  33749  poimirlem18  33783  poimirlem21  33786  2reu5a  41780  reuan  41783  2reurex  41784  2rexreu  41788  2reu1  41789
  Copyright terms: Public domain W3C validator