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 2916
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 2911 . 2 wff ∃*𝑥𝐴 𝜑
52cv 1479 . . . . 5 class 𝑥
65, 3wcel 1987 . . . 4 wff 𝑥𝐴
76, 1wa 384 . . 3 wff (𝑥𝐴𝜑)
87, 2wmo 2470 . 2 wff ∃*𝑥(𝑥𝐴𝜑)
94, 8wb 196 1 wff (∃*𝑥𝐴 𝜑 ↔ ∃*𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  nfrmo1  3105  nfrmod  3107  nfrmo  3109  rmobida  3122  rmobiia  3125  rmoeq1f  3130  mormo  3151  reu5  3152  rmo5  3155  rmov  3212  rmo4  3386  rmoeq  3392  rmoan  3393  rmoim  3394  rmoimi2  3396  2reuswap  3397  2reu5lem2  3401  rmo2  3512  rmo3  3514  rmob  3515  rmob2  3517  dfdisj2  4595  reuxfr2d  4861  rmorabex  4899  dffun9  5886  fncnv  5930  iunmapdisj  8806  brdom4  9312  enqeq  9716  2ndcdisj  21199  2ndcdisj2  21200  pjhtheu  28141  pjpreeq  28145  cnlnadjeui  28824  rmoxfrd  29222  ssrmo  29223  rmo3f  29224  cbvdisjf  29271  funcnvmpt  29352  cdleme0moN  35031  2rmoswap  40518
  Copyright terms: Public domain W3C validator