MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-rmo Unicode version

Definition df-rmo 2564
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  set  x
3 cA . . 3  class  A
41, 2, 3wrmo 2559 . 2  wff  E* x  e.  A ph
52cv 1631 . . . . 5  class  x
65, 3wcel 1696 . . . 4  wff  x  e.  A
76, 1wa 358 . . 3  wff  ( x  e.  A  /\  ph )
87, 2wmo 2157 . 2  wff  E* x
( x  e.  A  /\  ph )
94, 8wb 176 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  2724  nfrmod  2726  nfrmo  2728  rmobida  2740  rmobiia  2743  rmoeq1f  2748  mormo  2765  reu5  2766  rmo5  2769  rmov  2817  rmo4  2971  rmoan  2976  rmoim  2977  rmoimi2  2979  2reuswap  2980  2reu5lem2  2984  rmo2  3089  rmo3  3091  rmob  3092  dfdisj2  4011  nfdisj  4021  invdisj  4028  rmorabex  4249  reuxfr2d  4573  dffun9  5298  fncnv  5330  iunmapdisj  7666  brdom4  8171  enqeq  8574  spwmo  14351  2ndcdisj  17198  2ndcdisj2  17199  pjhtheu  21989  pjpreeq  21993  cnlnadjeui  22673  rmoxfrd  23163  ssrmo  23164  rmo3f  23194  funcnvmpt  23250  cbvdisjf  23365  2rmoswap  28065  cdleme0moN  31036
  Copyright terms: Public domain W3C validator