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

Theorem reu5 3382
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 2569 . 2 (∃!𝑥(𝑥𝐴𝜑) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ ∃*𝑥(𝑥𝐴𝜑)))
2 df-reu 3381 . 2 (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))
3 df-rex 3071 . . 3 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
4 df-rmo 3380 . . 3 (∃*𝑥𝐴 𝜑 ↔ ∃*𝑥(𝑥𝐴𝜑))
53, 4anbi12i 628 . 2 ((∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ ∃*𝑥(𝑥𝐴𝜑)))
61, 2, 53bitr4i 303 1 (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  wex 1779  wcel 2108  ∃*wmo 2538  ∃!weu 2568  wrex 3070  ∃!wreu 3378  ∃*wrmo 3379
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 207  df-an 396  df-eu 2569  df-rex 3071  df-rmo 3380  df-reu 3381
This theorem is referenced by:  reurmo  3383  reurex  3384  cbvreuw  3410  reueq1  3417  reueq1f  3425  reu4  3737  reueq  3743  2reu5a  3750  2reurex  3766  2rexreu  3768  reuan  3896  2reu1  3897  reusv1  5397  wereu  5681  wereu2  5682  fncnv  6639  moriotass  7420  supeu  9494  infeu  9536  ttrcltr  9756  resqreu  15291  sqrtneg  15306  sqreu  15399  catideu  17718  poslubd  18458  ismgmid  18678  mndideu  18758  frlmup4  21821  evlseu  22107  ply1divalg  26177  2sqreulem1  27490  2sqreunnlem1  27493  nosupno  27748  nosupbday  27750  nosupbnd1  27759  nosupbnd2  27761  noinfno  27763  noinfbday  27765  noinfbnd1  27774  noinfbnd2  27776  noreceuw  28217  tglinethrueu  28647  foot  28730  mideu  28746  nbusgredgeu  29383  pjhtheu  31413  pjpreeq  31417  cnlnadjeui  32096  cvmliftlem14  35302  cvmlift2lem13  35320  cvmlift3  35333  r1peuqusdeg1  35648  linethrueu  36157  phpreu  37611  poimirlem18  37645  poimirlem21  37648  primrootsunit1  42098  addinvcom  42461  reutruALT  48725  lubeldm2  48853  glbeldm2  48854  upeu  48928
  Copyright terms: Public domain W3C validator