MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-rmo Structured version   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  4738  dffun9  5473  fncnv  5507  iunmapdisj  7896  brdom4  8400  enqeq  8803  spwmo  14650  2ndcdisj  17511  2ndcdisj2  17512  pjhtheu  22888  pjpreeq  22892  cnlnadjeui  23572  rmoxfrd  23972  ssrmo  23973  rmo3f  23974  cbvdisjf  24007  funcnvmpt  24075  2rmoswap  27929  cdleme0moN  30959
  Copyright terms: Public domain W3C validator