![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-riota | Unicode version |
Description: Define restricted
description binder. In case there is no unique ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
df-riota |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph |
. . 3
![]() ![]() | |
2 | vx |
. . 3
![]() ![]() | |
3 | cA |
. . 3
![]() ![]() | |
4 | 1, 2, 3 | crio 5843 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2 | cv 1362 |
. . . . 5
![]() ![]() |
6 | 5, 3 | wcel 2158 |
. . . 4
![]() ![]() ![]() ![]() |
7 | 6, 1 | wa 104 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 7, 2 | cio 5188 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 4, 8 | wceq 1363 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: riotaeqdv 5845 riotabidv 5846 riotaexg 5848 riotav 5849 riotauni 5850 nfriota1 5851 nfriotadxy 5852 cbvriota 5854 riotacl2 5857 riotabidva 5860 riota1 5862 riota2df 5864 snriota 5873 riotaund 5878 grpidvalg 12811 fn0g 12813 ismgmid 12815 oppr1g 13330 bdcriota 14931 |
Copyright terms: Public domain | W3C validator |