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 3111
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 3106 . 2 wff ∃*𝑥𝐴 𝜑
52cv 1636 . . . . 5 class 𝑥
65, 3wcel 2157 . . . 4 wff 𝑥𝐴
76, 1wa 384 . . 3 wff (𝑥𝐴𝜑)
87, 2wmo 2633 . 2 wff ∃*𝑥(𝑥𝐴𝜑)
94, 8wb 197 1 wff (∃*𝑥𝐴 𝜑 ↔ ∃*𝑥(𝑥𝐴𝜑))
Colors of variables: wff setvar class
This definition is referenced by:  rmoanid  3116  nfrmo1  3306  nfrmod  3308  nfrmo  3310  rmobida  3325  rmobiia  3328  rmoeq1f  3333  mormo  3354  reu5  3355  rmo5  3358  rmov  3423  rmo4  3604  rmoeq  3610  rmoan  3611  rmoim  3612  rmoimi2  3614  2reuswap  3615  2reu5lem2  3619  rmo2  3728  rmo3  3730  rmob  3731  rmob2  3733  dfdisj2  4821  reuxfr2d  5095  rmorabex  5125  dffun9  6133  fncnv  6176  iunmapdisj  9132  brdom4  9640  enqeq  10044  2ndcdisj  21477  2ndcdisj2  21478  pjhtheu  28587  pjpreeq  28591  cnlnadjeui  29270  rmoxfrd  29665  ssrmo  29666  rmo3f  29667  cbvdisjf  29716  funcnvmpt  29801  alrmomorn  34438  alrmomodm  34439  cdleme0moN  36007  2rmoswap  41697
  Copyright terms: Public domain W3C validator