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

Definition df-rmo 2705
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 2700 . 2  wff  E* x  e.  A ph
52cv 1651 . . . . 5  class  x
65, 3wcel 1725 . . . 4  wff  x  e.  A
76, 1wa 359 . . 3  wff  ( x  e.  A  /\  ph )
87, 2wmo 2281 . 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  2871  nfrmod  2873  nfrmo  2875  rmobida  2887  rmobiia  2890  rmoeq1f  2895  mormo  2912  reu5  2913  rmo5  2916  rmov  2964  rmo4  3119  rmoan  3124  rmoim  3125  rmoimi2  3127  2reuswap  3128  2reu5lem2  3132  rmo2  3238  rmo3  3240  rmob  3241  dfdisj2  4176  rmorabex  4415  reuxfr2d  4737  dffun9  5472  fncnv  5506  iunmapdisj  7893  brdom4  8397  enqeq  8800  spwmo  14646  2ndcdisj  17507  2ndcdisj2  17508  pjhtheu  22884  pjpreeq  22888  cnlnadjeui  23568  rmoxfrd  23968  ssrmo  23969  rmo3f  23970  cbvdisjf  24003  funcnvmpt  24071  2rmoswap  27876  cdleme0moN  30861
  Copyright terms: Public domain W3C validator