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

Definition df-rmo 2551
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 2546 . 2  wff  E* x  e.  A ph
52cv 1622 . . . . 5  class  x
65, 3wcel 1684 . . . 4  wff  x  e.  A
76, 1wa 358 . . 3  wff  ( x  e.  A  /\  ph )
87, 2wmo 2144 . 2  wff  E* x
( x  e.  A  /\  ph )
94, 8wb 176 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  2711  nfrmod  2713  nfrmo  2715  rmobida  2727  rmobiia  2730  rmoeq1f  2735  mormo  2752  reu5  2753  rmo5  2756  rmov  2804  rmo4  2958  rmoan  2963  rmoim  2964  rmoimi2  2966  2reuswap  2967  2reu5lem2  2971  rmo2  3076  rmo3  3078  rmob  3079  dfdisj2  3995  nfdisj  4005  invdisj  4012  rmorabex  4233  reuxfr2d  4557  dffun9  5282  fncnv  5314  iunmapdisj  7650  brdom4  8155  enqeq  8558  spwmo  14335  2ndcdisj  17182  2ndcdisj2  17183  pjhtheu  21973  pjpreeq  21977  cnlnadjeui  22657  rmoxfrd  23147  ssrmo  23148  rmo3f  23178  funcnvmpt  23235  cbvdisjf  23350  2rmoswap  27962  cdleme0moN  30414
  Copyright terms: Public domain W3C validator