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

Definition df-rmo 3056
Description: Define restricted "at most one". (Contributed by NM, 16-Jun-2017.)
Assertion
Ref Expression
df-rmo (∃*𝑥𝐴 𝜑 ↔ ∃*𝑥(𝑥𝐴𝜑))

Detailed syntax breakdown of Definition df-rmo
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
3 cA . . 3 class 𝐴
41, 2, 3wrmo 3051 . 2 wff ∃*𝑥𝐴 𝜑
52cv 1629 . . . . 5 class 𝑥
65, 3wcel 2137 . . . 4 wff 𝑥𝐴
76, 1wa 383 . . 3 wff (𝑥𝐴𝜑)
87, 2wmo 2606 . 2 wff ∃*𝑥(𝑥𝐴𝜑)
94, 8wb 196 1 wff (∃*𝑥𝐴 𝜑 ↔ ∃*𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  nfrmo1  3247  nfrmod  3249  nfrmo  3251  rmobida  3266  rmobiia  3269  rmoeq1f  3274  mormo  3295  reu5  3296  rmo5  3299  rmov  3360  rmo4  3538  rmoeq  3544  rmoan  3545  rmoim  3546  rmoimi2  3548  2reuswap  3549  2reu5lem2  3553  rmo2  3665  rmo3  3667  rmob  3668  rmob2  3670  dfdisj2  4772  reuxfr2d  5038  rmorabex  5075  dffun9  6076  fncnv  6121  iunmapdisj  9034  brdom4  9542  enqeq  9946  2ndcdisj  21459  2ndcdisj2  21460  pjhtheu  28560  pjpreeq  28564  cnlnadjeui  29243  rmoxfrd  29639  ssrmo  29640  rmo3f  29641  cbvdisjf  29690  funcnvmpt  29775  alrmomorn  34444  alrmomodm  34445  cdleme0moN  36013  2rmoswap  41688
  Copyright terms: Public domain W3C validator