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

Definition df-rmo 2368
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 2363 . 2 wff ∃*𝑥𝐴 𝜑
52cv 1289 . . . . 5 class 𝑥
65, 3wcel 1439 . . . 4 wff 𝑥𝐴
76, 1wa 103 . . 3 wff (𝑥𝐴𝜑)
87, 2wmo 1950 . 2 wff ∃*𝑥(𝑥𝐴𝜑)
94, 8wb 104 1 wff (∃*𝑥𝐴 𝜑 ↔ ∃*𝑥(𝑥𝐴𝜑))
Colors of variables: wff set class
This definition is referenced by:  nfrmo1  2540  rmobida  2554  rmobiia  2557  rmoeq1f  2562  mormo  2579  reu5  2580  rmo5  2583  rmov  2640  rmo4  2809  rmo3f  2813  rmoan  2816  rmoim  2817  rmoimi2  2819  2reuswapdc  2820  2rmorex  2822  rmo2ilem  2929  rmo3  2931  rmob  2932  dfdisj2  3830  dffun9  5057  fncnv  5093
  Copyright terms: Public domain W3C validator