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

Definition df-rmo 2713
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 2708 . 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 2282 . 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  2879  nfrmod  2881  nfrmo  2883  rmobida  2895  rmobiia  2898  rmoeq1f  2903  mormo  2920  reu5  2921  rmo5  2924  rmov  2972  rmo4  3127  rmoan  3132  rmoim  3133  rmoimi2  3135  2reuswap  3136  2reu5lem2  3140  rmo2  3246  rmo3  3248  rmob  3249  dfdisj2  4184  rmorabex  4423  reuxfr2d  4746  dffun9  5481  fncnv  5515  iunmapdisj  7904  brdom4  8408  enqeq  8811  spwmo  14658  2ndcdisj  17519  2ndcdisj2  17520  pjhtheu  22896  pjpreeq  22900  cnlnadjeui  23580  rmoxfrd  23980  ssrmo  23981  rmo3f  23982  cbvdisjf  24015  funcnvmpt  24083  2rmoswap  27938  cdleme0moN  31022
  Copyright terms: Public domain W3C validator