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

Definition df-rmo 2331
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 2326 . 2  wff  E* x  e.  A  ph
52cv 1258 . . . . 5  class  x
65, 3wcel 1409 . . . 4  wff  x  e.  A
76, 1wa 101 . . 3  wff  ( x  e.  A  /\  ph )
87, 2wmo 1917 . 2  wff  E* x
( x  e.  A  /\  ph )
94, 8wb 102 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  2499  rmobida  2513  rmobiia  2516  rmoeq1f  2521  mormo  2538  reu5  2539  rmo5  2542  rmov  2591  rmo4  2756  rmoan  2761  rmoim  2762  rmoimi2  2764  2reuswapdc  2765  2rmorex  2767  rmo2ilem  2874  rmo3  2876  rmob  2877  dfdisj2  3774  dffun9  4957  fncnv  4992
  Copyright terms: Public domain W3C validator