![]() |
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > NFE 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 2617 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2 | cv 1641 |
. . . . 5
![]() ![]() |
6 | 5, 3 | wcel 1710 |
. . . 4
![]() ![]() ![]() ![]() |
7 | 6, 1 | wa 358 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 7, 2 | wmo 2205 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 4, 8 | wb 176 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
This definition is referenced by: nfrmo1 2782 nfrmod 2784 nfrmo 2786 rmobida 2798 rmobiia 2801 rmoeq1f 2806 mormo 2823 reu5 2824 rmo5 2827 rmov 2875 rmo4 3029 rmoan 3034 rmoim 3035 rmoimi2 3037 2reuswap 3038 2reu5lem2 3042 rmo2 3131 rmo3 3133 rmob 3134 fncnv 5158 |
Copyright terms: Public domain | W3C validator |