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

Definition df-rmo 2815
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
2 vx . . 3
3 cA . . 3
41, 2, 3wrmo 2810 . 2
52cv 1394 . . . . 5
65, 3wcel 1818 . . . 4
76, 1wa 369 . . 3
87, 2wmo 2283 . 2
94, 8wb 184 1
Colors of variables: wff setvar class
This definition is referenced by:  nfrmo1  3029  nfrmod  3031  nfrmo  3033  rmobida  3045  rmobiia  3048  rmoeq1f  3053  mormo  3072  reu5  3073  rmo5  3076  rmov  3126  rmo4  3292  rmoan  3298  rmoim  3299  rmoimi2  3301  2reuswap  3302  2reu5lem2  3306  rmo2  3427  rmo3  3429  rmob  3430  rmob2  3432  dfdisj2  4424  reuxfr2d  4675  rmorabex  4712  dffun9  5621  fncnv  5657  iunmapdisj  8425  brdom4  8929  enqeq  9333  2ndcdisj  19957  2ndcdisj2  19958  pjhtheu  26312  pjpreeq  26316  cnlnadjeui  26996  rmoxfrd  27392  ssrmo  27393  rmo3f  27394  cbvdisjf  27434  funcnvmpt  27510  2rmoswap  32189  cdleme0moN  35950
  Copyright terms: Public domain W3C validator