![]() |
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 2420 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2 | cv 1331 |
. . . . 5
![]() ![]() |
6 | 5, 3 | wcel 1481 |
. . . 4
![]() ![]() ![]() ![]() |
7 | 6, 1 | wa 103 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 7, 2 | wmo 2001 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 4, 8 | wb 104 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: nfrmo1 2606 rmobida 2620 rmobiia 2623 rmoeq1f 2628 mormo 2645 reu5 2646 rmo5 2649 rmov 2709 rmo4 2881 rmo3f 2885 rmoan 2888 rmoim 2889 rmoimi2 2891 2reuswapdc 2892 2rmorex 2894 rmo2ilem 3002 rmo3 3004 rmob 3005 ssrmof 3165 dfdisj2 3916 dffun9 5160 fncnv 5197 |
Copyright terms: Public domain | W3C validator |