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

Definition df-rmo 2363
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 2358 . 2 wff ∃*𝑥𝐴 𝜑
52cv 1286 . . . . 5 class 𝑥
65, 3wcel 1436 . . . 4 wff 𝑥𝐴
76, 1wa 102 . . 3 wff (𝑥𝐴𝜑)
87, 2wmo 1946 . 2 wff ∃*𝑥(𝑥𝐴𝜑)
94, 8wb 103 1 wff (∃*𝑥𝐴 𝜑 ↔ ∃*𝑥(𝑥𝐴𝜑))
Colors of variables: wff set class
This definition is referenced by:  nfrmo1  2535  rmobida  2549  rmobiia  2552  rmoeq1f  2557  mormo  2574  reu5  2575  rmo5  2578  rmov  2633  rmo4  2799  rmoan  2804  rmoim  2805  rmoimi2  2807  2reuswapdc  2808  2rmorex  2810  rmo2ilem  2917  rmo3  2919  rmob  2920  dfdisj2  3805  dffun9  5011  fncnv  5047
  Copyright terms: Public domain W3C validator