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

Definition df-rmo 2480
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 2475 . 2  wff  E* x  e.  A  ph
52cv 1363 . . . . 5  class  x
65, 3wcel 2164 . . . 4  wff  x  e.  A
76, 1wa 104 . . 3  wff  ( x  e.  A  /\  ph )
87, 2wmo 2043 . 2  wff  E* x
( x  e.  A  /\  ph )
94, 8wb 105 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  2667  rmobida  2681  rmobiia  2684  rmoeq1f  2689  mormo  2710  reu5  2711  rmo5  2714  rmov  2780  rmo4  2953  rmo3f  2957  rmoan  2960  rmoim  2961  rmoimi2  2963  2reuswapdc  2964  2rmorex  2966  rmo2ilem  3075  rmo3  3077  rmob  3078  ssrmof  3242  dfdisj2  4008  dffun9  5283  fncnv  5320
  Copyright terms: Public domain W3C validator