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 3146
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 3143). (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 3141 . 2 wff ∃*𝑥𝐴 𝜑
52cv 1527 . . . . 5 class 𝑥
65, 3wcel 2105 . . . 4 wff 𝑥𝐴
76, 1wa 396 . . 3 wff (𝑥𝐴𝜑)
87, 2wmo 2616 . 2 wff ∃*𝑥(𝑥𝐴𝜑)
94, 8wb 207 1 wff (∃*𝑥𝐴 𝜑 ↔ ∃*𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  rmoanid  3329  nfrmo1  3372  nfrmod  3374  nfrmow  3376  nfrmo  3378  rmobida  3393  rmobiia  3396  rmoeq1f  3401  rmoeq1  3409  mormo  3430  reu5  3431  rmo5  3435  rmov  3523  rmo4  3720  rmo3f  3724  rmoeq  3728  rmoan  3729  rmoim  3730  rmoimi2  3733  2reuswap  3736  2reu5lem2  3746  2rmoswap  3751  rmo2  3869  rmo3  3871  rmo3OLD  3872  rmob  3873  rmob2  3875  rmoanim  3877  ssrmof  4031  dfdisj2  5025  rmorabex  5344  dffun9  6378  fncnv  6421  iunmapdisj  9438  brdom4  9941  enqeq  10345  2ndcdisj  21994  2ndcdisj2  21995  pjhtheu  29099  pjpreeq  29103  cnlnadjeui  29782  reuxfrdf  30183  rmoxfrd  30185  rmoun  30186  rmounid  30187  cbvdisjf  30250  funcnvmpt  30341  nrmo  33656  alrmomorn  35495  alrmomodm  35496  dfeldisj4  35835  cdleme0moN  37243
  Copyright terms: Public domain W3C validator