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 such that holds, it evaluates to the empty set. See also comments for df-iota 5158. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) (Revised by NM, 2-Sep-2018.) |
Ref | Expression |
---|---|
df-riota |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 | |
2 | vx | . . 3 | |
3 | cA | . . 3 | |
4 | 1, 2, 3 | crio 5805 | . 2 |
5 | 2 | cv 1347 | . . . . 5 |
6 | 5, 3 | wcel 2141 | . . . 4 |
7 | 6, 1 | wa 103 | . . 3 |
8 | 7, 2 | cio 5156 | . 2 |
9 | 4, 8 | wceq 1348 | 1 |
Colors of variables: wff set class |
This definition is referenced by: riotaeqdv 5807 riotabidv 5808 riotaexg 5810 riotav 5811 riotauni 5812 nfriota1 5813 nfriotadxy 5814 cbvriota 5816 riotacl2 5819 riotabidva 5822 riota1 5824 riota2df 5826 snriota 5835 riotaund 5840 grpidvalg 12614 fn0g 12616 ismgmid 12618 bdcriota 13878 |
Copyright terms: Public domain | W3C validator |