![]() |
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 2356 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2 | cv 1284 |
. . . . 5
![]() ![]() |
6 | 5, 3 | wcel 1434 |
. . . 4
![]() ![]() ![]() ![]() |
7 | 6, 1 | wa 102 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 7, 2 | wmo 1944 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 4, 8 | wb 103 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: nfrmo1 2531 rmobida 2545 rmobiia 2548 rmoeq1f 2553 mormo 2570 reu5 2571 rmo5 2574 rmov 2628 rmo4 2795 rmoan 2800 rmoim 2801 rmoimi2 2803 2reuswapdc 2804 2rmorex 2806 rmo2ilem 2913 rmo3 2915 rmob 2916 dfdisj2 3789 dffun9 4981 fncnv 5017 |
Copyright terms: Public domain | W3C validator |