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

Definition df-rmo 2476
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 2471 . 2 wff ∃*𝑥𝐴 𝜑
52cv 1363 . . . . 5 class 𝑥
65, 3wcel 2160 . . . 4 wff 𝑥𝐴
76, 1wa 104 . . 3 wff (𝑥𝐴𝜑)
87, 2wmo 2039 . 2 wff ∃*𝑥(𝑥𝐴𝜑)
94, 8wb 105 1 wff (∃*𝑥𝐴 𝜑 ↔ ∃*𝑥(𝑥𝐴𝜑))
Colors of variables: wff set class
This definition is referenced by:  nfrmo1  2663  rmobida  2677  rmobiia  2680  rmoeq1f  2685  mormo  2702  reu5  2703  rmo5  2706  rmov  2772  rmo4  2945  rmo3f  2949  rmoan  2952  rmoim  2953  rmoimi2  2955  2reuswapdc  2956  2rmorex  2958  rmo2ilem  3067  rmo3  3069  rmob  3070  ssrmof  3233  dfdisj2  3997  dffun9  5264  fncnv  5301
  Copyright terms: Public domain W3C validator