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

Theorem reu5 3298
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 2633 . 2 (∃!𝑥(𝑥𝐴𝜑) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ ∃*𝑥(𝑥𝐴𝜑)))
2 df-reu 3057 . 2 (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))
3 df-rex 3056 . . 3 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
4 df-rmo 3058 . . 3 (∃*𝑥𝐴 𝜑 ↔ ∃*𝑥(𝑥𝐴𝜑))
53, 4anbi12i 735 . 2 ((∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ ∃*𝑥(𝑥𝐴𝜑)))
61, 2, 53bitr4i 292 1 (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383  wex 1853  wcel 2139  ∃!weu 2607  ∃*wmo 2608  wrex 3051  ∃!wreu 3052  ∃*wrmo 3053
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-eu 2611  df-mo 2612  df-rex 3056  df-reu 3057  df-rmo 3058
This theorem is referenced by:  reurex  3299  reurmo  3300  reu4  3541  reueq  3545  reusv1  5015  reusv1OLD  5016  wereu  5262  wereu2  5263  fncnv  6123  moriotass  6803  supeu  8525  infeu  8567  resqreu  14192  sqrtneg  14207  sqreu  14299  catideu  16537  poslubd  17349  ismgmid  17465  mndideu  17505  evlseu  19718  frlmup4  20342  ply1divalg  24096  tglinethrueu  25733  foot  25813  mideu  25829  nbusgredgeu  26466  pjhtheu  28562  pjpreeq  28566  cnlnadjeui  29245  cvmliftlem14  31586  cvmlift2lem13  31604  cvmlift3  31617  nosupno  32155  nosupbday  32157  nosupbnd1  32166  nosupbnd2  32168  linethrueu  32569  phpreu  33706  poimirlem18  33740  poimirlem21  33743  2reu5a  41683  reuan  41686  2reurex  41687  2rexreu  41691  2reu1  41692
  Copyright terms: Public domain W3C validator