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

Definition df-rmo 2456
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 2451 . 2 wff ∃*𝑥𝐴 𝜑
52cv 1347 . . . . 5 class 𝑥
65, 3wcel 2141 . . . 4 wff 𝑥𝐴
76, 1wa 103 . . 3 wff (𝑥𝐴𝜑)
87, 2wmo 2020 . 2 wff ∃*𝑥(𝑥𝐴𝜑)
94, 8wb 104 1 wff (∃*𝑥𝐴 𝜑 ↔ ∃*𝑥(𝑥𝐴𝜑))
Colors of variables: wff set class
This definition is referenced by:  nfrmo1  2642  rmobida  2656  rmobiia  2659  rmoeq1f  2664  mormo  2681  reu5  2682  rmo5  2685  rmov  2750  rmo4  2923  rmo3f  2927  rmoan  2930  rmoim  2931  rmoimi2  2933  2reuswapdc  2934  2rmorex  2936  rmo2ilem  3044  rmo3  3046  rmob  3047  ssrmof  3210  dfdisj2  3966  dffun9  5225  fncnv  5262
  Copyright terms: Public domain W3C validator