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 2949
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 2944 . 2 wff ∃*𝑥𝐴 𝜑
52cv 1522 . . . . 5 class 𝑥
65, 3wcel 2030 . . . 4 wff 𝑥𝐴
76, 1wa 383 . . 3 wff (𝑥𝐴𝜑)
87, 2wmo 2499 . 2 wff ∃*𝑥(𝑥𝐴𝜑)
94, 8wb 196 1 wff (∃*𝑥𝐴 𝜑 ↔ ∃*𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  nfrmo1  3140  nfrmod  3142  nfrmo  3144  rmobida  3159  rmobiia  3162  rmoeq1f  3167  mormo  3188  reu5  3189  rmo5  3192  rmov  3253  rmo4  3432  rmoeq  3438  rmoan  3439  rmoim  3440  rmoimi2  3442  2reuswap  3443  2reu5lem2  3447  rmo2  3559  rmo3  3561  rmob  3562  rmob2  3564  dfdisj2  4654  reuxfr2d  4921  rmorabex  4958  dffun9  5955  fncnv  6000  iunmapdisj  8884  brdom4  9390  enqeq  9794  2ndcdisj  21307  2ndcdisj2  21308  pjhtheu  28381  pjpreeq  28385  cnlnadjeui  29064  rmoxfrd  29460  ssrmo  29461  rmo3f  29462  cbvdisjf  29511  funcnvmpt  29596  alrmomorn  34263  alrmomodm  34264  cdleme0moN  35830  2rmoswap  41505
  Copyright terms: Public domain W3C validator