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

Definition df-rmo 2554
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 2549 . 2  wff  E* x  e.  A ph
52cv 1624 . . . . 5  class  x
65, 3wcel 1687 . . . 4  wff  x  e.  A
76, 1wa 360 . . 3  wff  ( x  e.  A  /\  ph )
87, 2wmo 2147 . 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  2714  nfrmod  2716  nfrmo  2718  rmobida  2730  rmobiia  2733  rmoeq1f  2738  mormo  2755  reu5  2756  rmo5  2759  rmov  2807  rmo4  2961  rmoan  2966  rmoim  2967  rmoimi2  2969  2reuswap  2970  2reu5lem2  2974  rmo2  3079  rmo3  3081  rmob  3082  dfdisj2  3998  nfdisj  4008  invdisj  4015  rmorabex  4234  reuxfr2d  4558  dffun9  5250  fncnv  5281  iunmapdisj  7647  brdom4  8152  enqeq  8555  spwmo  14331  2ndcdisj  17178  2ndcdisj2  17179  pjhtheu  21967  pjpreeq  21971  cnlnadjeui  22651  2rmoswap  27343  cdleme0moN  29683
  Copyright terms: Public domain W3C validator