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 3380
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 3062). (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 3379 . 2 wff ∃*𝑥𝐴 𝜑
52cv 1539 . . . . 5 class 𝑥
65, 3wcel 2108 . . . 4 wff 𝑥𝐴
76, 1wa 395 . . 3 wff (𝑥𝐴𝜑)
87, 2wmo 2538 . 2 wff ∃*𝑥(𝑥𝐴𝜑)
94, 8wb 206 1 wff (∃*𝑥𝐴 𝜑 ↔ ∃*𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  reu5  3382  mormo  3385  rmobiia  3386  rmoanidOLD  3392  rmobidva  3395  rmo5  3400  cbvrmovw  3403  rmobida  3406  cbvrmow  3409  nfrmo1  3411  nfrmow  3413  rmoeq1  3416  rmoeq1OLD  3418  rmoeq1f  3424  nfrmowOLD  3427  nfrmod  3432  nfrmo  3434  rmov  3511  rmo4  3736  rmo3f  3740  rmoeq  3744  rmoan  3745  rmoim  3746  rmoimi2  3749  2reuswap  3752  2reu5lem2  3762  2rmoswap  3767  rmo2  3887  rmo3  3889  rmob  3890  rmob2  3892  rmoanim  3894  ssrmof  4051  dfdisj2  5112  rmorabex  5465  dffun9  6595  fncnv  6639  iunmapdisj  10063  brdom4  10570  enqeq  10974  2ndcdisj  23464  2ndcdisj2  23465  pjhtheu  31413  pjpreeq  31417  cnlnadjeui  32096  reuxfrdf  32510  rmoxfrd  32512  rmoun  32513  rmounid  32514  cbvdisjf  32584  funcnvmpt  32677  rmoeqi  36188  rmoeqbii  36189  rmoeqbidv  36214  disjeq12dv  36216  cbvrmovw2  36229  cbvrmodavw  36253  cbvrmodavw2  36284  nrmo  36411  alrmomorn  38359  alrmomodm  38360  dfeldisj4  38721  disjres  38745  cdleme0moN  40227  onsucf1olem  43283  tfsconcatlem  43349  modelaxreplem2  44996  rmotru  48723
  Copyright terms: Public domain W3C validator