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

Definition df-rmo 2401
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 2396 . 2  wff  E* x  e.  A  ph
52cv 1315 . . . . 5  class  x
65, 3wcel 1465 . . . 4  wff  x  e.  A
76, 1wa 103 . . 3  wff  ( x  e.  A  /\  ph )
87, 2wmo 1978 . 2  wff  E* x
( x  e.  A  /\  ph )
94, 8wb 104 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  2580  rmobida  2594  rmobiia  2597  rmoeq1f  2602  mormo  2619  reu5  2620  rmo5  2623  rmov  2680  rmo4  2850  rmo3f  2854  rmoan  2857  rmoim  2858  rmoimi2  2860  2reuswapdc  2861  2rmorex  2863  rmo2ilem  2970  rmo3  2972  rmob  2973  ssrmof  3130  dfdisj2  3878  dffun9  5122  fncnv  5159
  Copyright terms: Public domain W3C validator