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

Definition df-rmo 2674
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 2669 . 2  wff  E* x  e.  A ph
52cv 1648 . . . . 5  class  x
65, 3wcel 1721 . . . 4  wff  x  e.  A
76, 1wa 359 . . 3  wff  ( x  e.  A  /\  ph )
87, 2wmo 2255 . 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  2839  nfrmod  2841  nfrmo  2843  rmobida  2855  rmobiia  2858  rmoeq1f  2863  mormo  2880  reu5  2881  rmo5  2884  rmov  2932  rmo4  3087  rmoan  3092  rmoim  3093  rmoimi2  3095  2reuswap  3096  2reu5lem2  3100  rmo2  3206  rmo3  3208  rmob  3209  dfdisj2  4144  rmorabex  4383  reuxfr2d  4705  dffun9  5440  fncnv  5474  iunmapdisj  7860  brdom4  8364  enqeq  8767  spwmo  14613  2ndcdisj  17472  2ndcdisj2  17473  pjhtheu  22849  pjpreeq  22853  cnlnadjeui  23533  rmoxfrd  23933  ssrmo  23934  rmo3f  23935  cbvdisjf  23968  funcnvmpt  24036  2rmoswap  27829  cdleme0moN  30707
  Copyright terms: Public domain W3C validator