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

Theorem reu5 3148
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 2495 . 2 (∃!𝑥(𝑥𝐴𝜑) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ ∃*𝑥(𝑥𝐴𝜑)))
2 df-reu 2914 . 2 (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))
3 df-rex 2913 . . 3 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
4 df-rmo 2915 . . 3 (∃*𝑥𝐴 𝜑 ↔ ∃*𝑥(𝑥𝐴𝜑))
53, 4anbi12i 732 . 2 ((∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ ∃*𝑥(𝑥𝐴𝜑)))
61, 2, 53bitr4i 292 1 (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384  wex 1701  wcel 1987  ∃!weu 2469  ∃*wmo 2470  wrex 2908  ∃!wreu 2909  ∃*wrmo 2910
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-eu 2473  df-mo 2474  df-rex 2913  df-reu 2914  df-rmo 2915
This theorem is referenced by:  reurex  3149  reurmo  3150  reu4  3382  reueq  3386  reusv1  4826  reusv1OLD  4827  wereu  5070  wereu2  5071  fncnv  5920  moriotass  6594  supeu  8304  infeu  8346  resqreu  13927  sqrtneg  13942  sqreu  14034  catideu  16257  poslubd  17069  ismgmid  17185  mndideu  17225  evlseu  19435  frlmup4  20059  ply1divalg  23801  tglinethrueu  25434  foot  25514  mideu  25530  nbusgredgeu  26155  pjhtheu  28102  pjpreeq  28106  cnlnadjeui  28785  cvmliftlem14  30987  cvmlift2lem13  31005  cvmlift3  31018  nosino  31575  linethrueu  31905  phpreu  33025  poimirlem18  33059  poimirlem21  33062  2reu5a  40481  reuan  40484  2reurex  40485  2rexreu  40489  2reu1  40490
  Copyright terms: Public domain W3C validator