Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-rmo | Unicode version |
Description: Define restricted "at most one". (Contributed by NM, 16-Jun-2017.) |
Ref | Expression |
---|---|
df-rmo |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 | |
2 | vx | . . 3 | |
3 | cA | . . 3 | |
4 | 1, 2, 3 | wrmo 2419 | . 2 |
5 | 2 | cv 1330 | . . . . 5 |
6 | 5, 3 | wcel 1480 | . . . 4 |
7 | 6, 1 | wa 103 | . . 3 |
8 | 7, 2 | wmo 2000 | . 2 |
9 | 4, 8 | wb 104 | 1 |
Colors of variables: wff set class |
This definition is referenced by: nfrmo1 2603 rmobida 2617 rmobiia 2620 rmoeq1f 2625 mormo 2642 reu5 2643 rmo5 2646 rmov 2706 rmo4 2877 rmo3f 2881 rmoan 2884 rmoim 2885 rmoimi2 2887 2reuswapdc 2888 2rmorex 2890 rmo2ilem 2998 rmo3 3000 rmob 3001 ssrmof 3160 dfdisj2 3908 dffun9 5152 fncnv 5189 |
Copyright terms: Public domain | W3C validator |