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 2396 | . 2 |
5 | 2 | cv 1315 | . . . . 5 |
6 | 5, 3 | wcel 1465 | . . . 4 |
7 | 6, 1 | wa 103 | . . 3 |
8 | 7, 2 | wmo 1978 | . 2 |
9 | 4, 8 | wb 104 | 1 |
Colors of variables: wff set class |
This definition is referenced by: nfrmo1 2580 rmobida 2594 rmobiia 2597 rmoeq1f 2602 mormo 2619 reu5 2620 rmo5 2623 rmov 2680 rmo4 2850 rmo3f 2854 rmoan 2857 rmoim 2858 rmoimi2 2860 2reuswapdc 2861 2rmorex 2863 rmo2ilem 2970 rmo3 2972 rmob 2973 ssrmof 3130 dfdisj2 3878 dffun9 5122 fncnv 5159 |
Copyright terms: Public domain | W3C validator |