![]() |
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 2303 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2 | cv 1241 |
. . . . 5
![]() ![]() |
6 | 5, 3 | wcel 1390 |
. . . 4
![]() ![]() ![]() ![]() |
7 | 6, 1 | wa 97 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 7, 2 | wmo 1898 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 4, 8 | wb 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 |