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

Definition df-rmo 2650
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 2645 . 2  wff  E* x  e.  A ph
52cv 1648 . . . . 5  class  x
65, 3wcel 1717 . . . 4  wff  x  e.  A
76, 1wa 359 . . 3  wff  ( x  e.  A  /\  ph )
87, 2wmo 2232 . 2  wff  E* x
( x  e.  A  /\  ph )
94, 8wb 177 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  2815  nfrmod  2817  nfrmo  2819  rmobida  2831  rmobiia  2834  rmoeq1f  2839  mormo  2856  reu5  2857  rmo5  2860  rmov  2908  rmo4  3063  rmoan  3068  rmoim  3069  rmoimi2  3071  2reuswap  3072  2reu5lem2  3076  rmo2  3182  rmo3  3184  rmob  3185  dfdisj2  4118  rmorabex  4357  reuxfr2d  4679  dffun9  5414  fncnv  5448  iunmapdisj  7830  brdom4  8334  enqeq  8737  spwmo  14578  2ndcdisj  17433  2ndcdisj2  17434  pjhtheu  22737  pjpreeq  22741  cnlnadjeui  23421  rmoxfrd  23817  ssrmo  23818  rmo3f  23819  cbvdisjf  23852  funcnvmpt  23917  2rmoswap  27623  cdleme0moN  30390
  Copyright terms: Public domain W3C validator