ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-rmo Structured version   Unicode version

Definition df-rmo 2308
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  setvar
3 cA . . 3
41, 2, 3wrmo 2303 . 2
52cv 1241 . . . . 5
65, 3wcel 1390 . . . 4
76, 1wa 97 . . 3
87, 2wmo 1898 . 2
94, 8wb 98 1
Colors of variables: wff set class
This definition is referenced by:  nfrmo1  2476  rmobida  2490  rmobiia  2493  rmoeq1f  2498  mormo  2515  reu5  2516  rmo5  2519  rmov  2568  rmo4  2728  rmoan  2733  rmoim  2734  rmoimi2  2736  2reuswapdc  2737  2rmorex  2739  rmo2ilem  2841  rmo3  2843  rmob  2844  dfdisj2  3738  dffun9  4873  fncnv  4908
  Copyright terms: Public domain W3C validator