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

Definition df-rmo 2363
Description: Define restricted "at most one". (Contributed by NM, 16-Jun-2017.)
Assertion
Ref Expression
df-rmo  |-  ( E* x  e.  A  ph  <->  E* x ( x  e.  A  /\  ph )
)

Detailed syntax breakdown of Definition df-rmo
StepHypRef Expression
1 wph . . 3  wff  ph
2 vx . . 3  setvar  x
3 cA . . 3  class  A
41, 2, 3wrmo 2358 . 2  wff  E* x  e.  A  ph
52cv 1286 . . . . 5  class  x
65, 3wcel 1436 . . . 4  wff  x  e.  A
76, 1wa 102 . . 3  wff  ( x  e.  A  /\  ph )
87, 2wmo 1946 . 2  wff  E* x
( x  e.  A  /\  ph )
94, 8wb 103 1  wff  ( E* x  e.  A  ph  <->  E* x ( x  e.  A  /\  ph )
)
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  3803  dffun9  5009  fncnv  5045
  Copyright terms: Public domain W3C validator