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

Theorem reu5 3406
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 2653 . 2 (∃!𝑥(𝑥𝐴𝜑) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ ∃*𝑥(𝑥𝐴𝜑)))
2 df-reu 3132 . 2 (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))
3 df-rex 3131 . . 3 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
4 df-rmo 3133 . . 3 (∃*𝑥𝐴 𝜑 ↔ ∃*𝑥(𝑥𝐴𝜑))
53, 4anbi12i 628 . 2 ((∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ ∃*𝑥(𝑥𝐴𝜑)))
61, 2, 53bitr4i 305 1 (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 208  wa 398  wex 1780  wcel 2114  ∃*wmo 2620  ∃!weu 2652  wrex 3126  ∃!wreu 3127  ∃*wrmo 3128
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 209  df-an 399  df-eu 2653  df-rex 3131  df-reu 3132  df-rmo 3133
This theorem is referenced by:  reurex  3407  reurmo  3409  reu4  3698  reueq  3704  2reu5a  3711  2reurex  3726  2rexreu  3729  reuan  3853  2reu1  3854  reusv1  5270  wereu  5523  wereu2  5524  fncnv  6399  moriotass  7119  supeu  8892  infeu  8934  resqreu  14588  sqrtneg  14603  sqreu  14696  catideu  16921  poslubd  17733  ismgmid  17850  mndideu  17897  evlseu  20268  frlmup4  20917  ply1divalg  24713  2sqreulem1  26005  2sqreunnlem1  26008  tglinethrueu  26408  foot  26491  mideu  26507  nbusgredgeu  27131  pjhtheu  29152  pjpreeq  29156  cnlnadjeui  29835  cvmliftlem14  32548  cvmlift2lem13  32566  cvmlift3  32579  nosupno  33207  nosupbday  33209  nosupbnd1  33218  nosupbnd2  33220  linethrueu  33621  phpreu  34913  poimirlem18  34947  poimirlem21  34950  addinvcom  39375
  Copyright terms: Public domain W3C validator