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

Definition df-rmo 2715
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 2710 . 2  wff  E* x  e.  A ph
52cv 1652 . . . . 5  class  x
65, 3wcel 1726 . . . 4  wff  x  e.  A
76, 1wa 360 . . 3  wff  ( x  e.  A  /\  ph )
87, 2wmo 2284 . 2  wff  E* x
( x  e.  A  /\  ph )
94, 8wb 178 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  2881  nfrmod  2883  nfrmo  2885  rmobida  2897  rmobiia  2900  rmoeq1f  2905  mormo  2922  reu5  2923  rmo5  2926  rmov  2974  rmo4  3129  rmoan  3134  rmoim  3135  rmoimi2  3137  2reuswap  3138  2reu5lem2  3142  rmo2  3248  rmo3  3250  rmob  3251  dfdisj2  4187  rmorabex  4426  reuxfr2d  4749  dffun9  5484  fncnv  5518  iunmapdisj  7909  brdom4  8413  enqeq  8816  spwmo  14663  2ndcdisj  17524  2ndcdisj2  17525  pjhtheu  22901  pjpreeq  22905  cnlnadjeui  23585  rmoxfrd  23985  ssrmo  23986  rmo3f  23987  cbvdisjf  24020  funcnvmpt  24088  2rmoswap  27952  cdleme0moN  31096
  Copyright terms: Public domain W3C validator