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 3150
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 3147). (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 3145 . 2 wff ∃*𝑥𝐴 𝜑
52cv 1529 . . . . 5 class 𝑥
65, 3wcel 2107 . . . 4 wff 𝑥𝐴
76, 1wa 396 . . 3 wff (𝑥𝐴𝜑)
87, 2wmo 2617 . 2 wff ∃*𝑥(𝑥𝐴𝜑)
94, 8wb 207 1 wff (∃*𝑥𝐴 𝜑 ↔ ∃*𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  rmoanid  3333  nfrmo1  3376  nfrmod  3378  nfrmow  3380  nfrmo  3382  rmobida  3397  rmobiia  3400  rmoeq1f  3405  rmoeq1  3413  mormo  3434  reu5  3435  rmo5  3439  rmov  3527  rmo4  3724  rmo3f  3728  rmoeq  3732  rmoan  3733  rmoim  3734  rmoimi2  3737  2reuswap  3740  2reu5lem2  3750  2rmoswap  3755  rmo2  3873  rmo3  3875  rmo3OLD  3876  rmob  3877  rmob2  3879  rmoanim  3881  ssrmof  4035  dfdisj2  5029  rmorabex  5348  dffun9  6380  fncnv  6423  iunmapdisj  9441  brdom4  9944  enqeq  10348  2ndcdisj  21983  2ndcdisj2  21984  pjhtheu  29088  pjpreeq  29092  cnlnadjeui  29771  reuxfrdf  30172  rmoxfrd  30174  rmoun  30175  rmounid  30176  cbvdisjf  30239  funcnvmpt  30330  nrmo  33645  alrmomorn  35483  alrmomodm  35484  dfeldisj4  35823  cdleme0moN  37231
  Copyright terms: Public domain W3C validator