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

Definition df-rmo 2331
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 2326 . 2 wff ∃*𝑥𝐴 𝜑
52cv 1258 . . . . 5 class 𝑥
65, 3wcel 1409 . . . 4 wff 𝑥𝐴
76, 1wa 101 . . 3 wff (𝑥𝐴𝜑)
87, 2wmo 1917 . 2 wff ∃*𝑥(𝑥𝐴𝜑)
94, 8wb 102 1 wff (∃*𝑥𝐴 𝜑 ↔ ∃*𝑥(𝑥𝐴𝜑))
Colors of variables: wff set class
This definition is referenced by:  nfrmo1  2499  rmobida  2513  rmobiia  2516  rmoeq1f  2521  mormo  2538  reu5  2539  rmo5  2542  rmov  2591  rmo4  2757  rmoan  2762  rmoim  2763  rmoimi2  2765  2reuswapdc  2766  2rmorex  2768  rmo2ilem  2875  rmo3  2877  rmob  2878  dfdisj2  3775  dffun9  4958  fncnv  4993
  Copyright terms: Public domain W3C validator