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

Definition df-rmo 2524
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 2519 . 2  wff  E* x  e.  A ph
52cv 1618 . . . . 5  class  x
65, 3wcel 1621 . . . 4  wff  x  e.  A
76, 1wa 360 . . 3  wff  ( x  e.  A  /\  ph )
87, 2wmo 2118 . 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  2684  nfrmod  2686  nfrmo  2688  rmobida  2700  rmobiia  2703  mormo  2722  reu5  2723  rmo5  2726  rmo4  2926  rmoan  2931  imrmo  2932  2reuswap  2933  rmo2  3037  rmo3  3039  rmob  3040  dfdisj2  3955  nfdisj  3965  invdisj  3972  rmorabex  4191  reuxfr2d  4515  dffun9  5207  fncnv  5238  iunmapdisj  7604  brdom4  8109  enqeq  8512  spwmo  14283  2ndcdisj  17130  2ndcdisj2  17131  pjhtheu  21919  pjpreeq  21923  cnlnadjeui  22603  cdleme0moN  29565
  Copyright terms: Public domain W3C validator