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

Definition df-rmo 2904
Description: Define restricted "at most one". (Contributed by NM, 16-Jun-2017.)
Assertion
Ref Expression
df-rmo (∃*𝑥𝐴 𝜑 ↔ ∃*𝑥(𝑥𝐴𝜑))

Detailed syntax breakdown of Definition df-rmo
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
3 cA . . 3 class 𝐴
41, 2, 3wrmo 2899 . 2 wff ∃*𝑥𝐴 𝜑
52cv 1474 . . . . 5 class 𝑥
65, 3wcel 1977 . . . 4 wff 𝑥𝐴
76, 1wa 383 . . 3 wff (𝑥𝐴𝜑)
87, 2wmo 2459 . 2 wff ∃*𝑥(𝑥𝐴𝜑)
94, 8wb 195 1 wff (∃*𝑥𝐴 𝜑 ↔ ∃*𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  nfrmo1  3090  nfrmod  3092  nfrmo  3094  rmobida  3106  rmobiia  3109  rmoeq1f  3114  mormo  3135  reu5  3136  rmo5  3139  rmov  3195  rmo4  3366  rmoeq  3372  rmoan  3373  rmoim  3374  rmoimi2  3376  2reuswap  3377  2reu5lem2  3381  rmo2  3492  rmo3  3494  rmob  3495  rmob2  3497  dfdisj2  4555  reuxfr2d  4817  rmorabex  4855  dffun9  5832  fncnv  5876  iunmapdisj  8729  brdom4  9233  enqeq  9635  2ndcdisj  21069  2ndcdisj2  21070  pjhtheu  27637  pjpreeq  27641  cnlnadjeui  28320  rmoxfrd  28717  ssrmo  28718  rmo3f  28719  cbvdisjf  28767  funcnvmpt  28851  cdleme0moN  34530  2rmoswap  39833
  Copyright terms: Public domain W3C validator