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

Definition df-rmo 2361
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 2356 . 2  wff  E* x  e.  A  ph
52cv 1284 . . . . 5  class  x
65, 3wcel 1434 . . . 4  wff  x  e.  A
76, 1wa 102 . . 3  wff  ( x  e.  A  /\  ph )
87, 2wmo 1944 . 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  2531  rmobida  2545  rmobiia  2548  rmoeq1f  2553  mormo  2570  reu5  2571  rmo5  2574  rmov  2628  rmo4  2795  rmoan  2800  rmoim  2801  rmoimi2  2803  2reuswapdc  2804  2rmorex  2806  rmo2ilem  2913  rmo3  2915  rmob  2916  dfdisj2  3789  dffun9  4981  fncnv  5017
  Copyright terms: Public domain W3C validator