NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-rmo GIF version

Definition df-rmo 2622
Description: Define restricted "at most one". (Contributed by NM, 16-Jun-2017.)
Assertion
Ref Expression
df-rmo (∃*x A φ∃*x(x A φ))

Detailed syntax breakdown of Definition df-rmo
StepHypRef Expression
1 wph . . 3 wff φ
2 vx . . 3 setvar x
3 cA . . 3 class A
41, 2, 3wrmo 2617 . 2 wff ∃*x A φ
52cv 1641 . . . . 5 class x
65, 3wcel 1710 . . . 4 wff x A
76, 1wa 358 . . 3 wff (x A φ)
87, 2wmo 2205 . 2 wff ∃*x(x A φ)
94, 8wb 176 1 wff (∃*x A φ∃*x(x A φ))
Colors of variables: wff setvar class
This definition is referenced by:  nfrmo1  2782  nfrmod  2784  nfrmo  2786  rmobida  2798  rmobiia  2801  rmoeq1f  2806  mormo  2823  reu5  2824  rmo5  2827  rmov  2875  rmo4  3029  rmoan  3034  rmoim  3035  rmoimi2  3037  2reuswap  3038  2reu5lem2  3042  rmo2  3131  rmo3  3133  rmob  3134  fncnv  5158
  Copyright terms: Public domain W3C validator