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 2903
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 2898 . 2 wff ∃*𝑥𝐴 𝜑
52cv 1473 . . . . 5 class 𝑥
65, 3wcel 1976 . . . 4 wff 𝑥𝐴
76, 1wa 382 . . 3 wff (𝑥𝐴𝜑)
87, 2wmo 2458 . 2 wff ∃*𝑥(𝑥𝐴𝜑)
94, 8wb 194 1 wff (∃*𝑥𝐴 𝜑 ↔ ∃*𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  nfrmo1  3089  nfrmod  3091  nfrmo  3093  rmobida  3105  rmobiia  3108  rmoeq1f  3113  mormo  3134  reu5  3135  rmo5  3138  rmov  3194  rmo4  3365  rmoeq  3371  rmoan  3372  rmoim  3373  rmoimi2  3375  2reuswap  3376  2reu5lem2  3380  rmo2  3491  rmo3  3493  rmob  3494  rmob2  3496  dfdisj2  4549  reuxfr2d  4811  rmorabex  4848  dffun9  5817  fncnv  5861  iunmapdisj  8706  brdom4  9210  enqeq  9612  2ndcdisj  21016  2ndcdisj2  21017  pjhtheu  27430  pjpreeq  27434  cnlnadjeui  28113  rmoxfrd  28510  ssrmo  28511  rmo3f  28512  cbvdisjf  28560  funcnvmpt  28644  cdleme0moN  34313  2rmoswap  39616
  Copyright terms: Public domain W3C validator