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

Definition df-rmo 3078
 Description: Define restricted "at most one". Note: This notation is most often used to express that 𝜑 holds for at most one element of a given class 𝐴. For this reading Ⅎ𝑥𝐴 is required, though, for example, asserted when 𝑥 and 𝐴 are disjoint. Should instead 𝐴 depend on 𝑥, you rather assert at most one 𝑥 fulfilling 𝜑 happens to be contained in the corresponding 𝐴(𝑥). This interpretation is rarely needed (see also df-ral 3075). (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 3073 . 2 wff ∃*𝑥𝐴 𝜑
52cv 1537 . . . . 5 class 𝑥
65, 3wcel 2111 . . . 4 wff 𝑥𝐴
76, 1wa 399 . . 3 wff (𝑥𝐴𝜑)
87, 2wmo 2555 . 2 wff ∃*𝑥(𝑥𝐴𝜑)
94, 8wb 209 1 wff (∃*𝑥𝐴 𝜑 ↔ ∃*𝑥(𝑥𝐴𝜑))
 Colors of variables: wff setvar class This definition is referenced by:  rmoanid  3252  nfrmo1  3289  nfrmod  3291  nfrmow  3293  nfrmo  3295  rmobida  3310  rmobiia  3313  rmoeq1f  3318  rmoeq1  3326  mormo  3339  reu5  3340  rmo5  3344  cbvrmow  3355  rmov  3438  rmo4  3644  rmo3f  3648  rmoeq  3652  rmoan  3653  rmoim  3654  rmoimi2  3657  2reuswap  3660  2reu5lem2  3670  2rmoswap  3675  rmo2  3793  rmo3  3795  rmob  3796  rmob2  3798  rmoanim  3800  ssrmof  3957  dfdisj2  4999  rmorabex  5320  dffun9  6364  fncnv  6408  iunmapdisj  9483  brdom4  9990  enqeq  10394  2ndcdisj  22156  2ndcdisj2  22157  pjhtheu  29276  pjpreeq  29280  cnlnadjeui  29959  reuxfrdf  30361  rmoxfrd  30363  rmoun  30364  rmounid  30365  cbvdisjf  30432  funcnvmpt  30528  nrmo  34148  alrmomorn  36052  alrmomodm  36053  dfeldisj4  36393  cdleme0moN  37801
 Copyright terms: Public domain W3C validator