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

Theorem reu5 3136
 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 2484 . 2 (∃!𝑥(𝑥𝐴𝜑) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ ∃*𝑥(𝑥𝐴𝜑)))
2 df-reu 2903 . 2 (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))
3 df-rex 2902 . . 3 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
4 df-rmo 2904 . . 3 (∃*𝑥𝐴 𝜑 ↔ ∃*𝑥(𝑥𝐴𝜑))
53, 4anbi12i 729 . 2 ((∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ ∃*𝑥(𝑥𝐴𝜑)))
61, 2, 53bitr4i 291 1 (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   ∧ wa 383  ∃wex 1695   ∈ wcel 1977  ∃!weu 2458  ∃*wmo 2459  ∃wrex 2897  ∃!wreu 2898  ∃*wrmo 2899 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875 This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-eu 2462  df-mo 2463  df-rex 2902  df-reu 2903  df-rmo 2904 This theorem is referenced by:  reurex  3137  reurmo  3138  reu4  3367  reueq  3371  reusv1  4792  reusv1OLD  4793  wereu  5034  wereu2  5035  fncnv  5876  moriotass  6539  supeu  8243  infeu  8285  resqreu  13841  sqrtneg  13856  sqreu  13948  catideu  16159  poslubd  16971  ismgmid  17087  mndideu  17127  evlseu  19337  frlmup4  19959  ply1divalg  23701  tglinethrueu  25334  foot  25414  mideu  25430  pjhtheu  27637  pjpreeq  27641  cnlnadjeui  28320  cvmliftlem14  30533  cvmlift2lem13  30551  cvmlift3  30564  linethrueu  31433  phpreu  32563  poimirlem18  32597  poimirlem21  32600  2reu5a  39826  reuan  39829  2reurex  39830  2rexreu  39834  2reu1  39835  nbusgredgeu  40594
 Copyright terms: Public domain W3C validator