![]() |
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 2475 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2 | cv 1363 |
. . . . 5
![]() ![]() |
6 | 5, 3 | wcel 2164 |
. . . 4
![]() ![]() ![]() ![]() |
7 | 6, 1 | wa 104 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 7, 2 | wmo 2043 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 4, 8 | wb 105 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: nfrmo1 2667 rmobida 2681 rmobiia 2684 rmoeq1f 2689 mormo 2710 reu5 2711 rmo5 2714 rmov 2780 rmo4 2953 rmo3f 2957 rmoan 2960 rmoim 2961 rmoimi2 2963 2reuswapdc 2964 2rmorex 2966 rmo2ilem 3075 rmo3 3077 rmob 3078 ssrmof 3242 dfdisj2 4008 dffun9 5283 fncnv 5320 |
Copyright terms: Public domain | W3C validator |