ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-rmo GIF version

Definition df-rmo 2314
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 2309 . 2 wff ∃*𝑥𝐴 𝜑
52cv 1242 . . . . 5 class 𝑥
65, 3wcel 1393 . . . 4 wff 𝑥𝐴
76, 1wa 97 . . 3 wff (𝑥𝐴𝜑)
87, 2wmo 1901 . 2 wff ∃*𝑥(𝑥𝐴𝜑)
94, 8wb 98 1 wff (∃*𝑥𝐴 𝜑 ↔ ∃*𝑥(𝑥𝐴𝜑))
Colors of variables: wff set class
This definition is referenced by:  nfrmo1  2482  rmobida  2496  rmobiia  2499  rmoeq1f  2504  mormo  2521  reu5  2522  rmo5  2525  rmov  2574  rmo4  2734  rmoan  2739  rmoim  2740  rmoimi2  2742  2reuswapdc  2743  2rmorex  2745  rmo2ilem  2847  rmo3  2849  rmob  2850  dfdisj2  3747  dffun9  4930  fncnv  4965
  Copyright terms: Public domain W3C validator