Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-riota | GIF 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 5160. (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 wff 𝜑 | |
2 | vx | . . 3 setvar 𝑥 | |
3 | cA | . . 3 class 𝐴 | |
4 | 1, 2, 3 | crio 5808 | . 2 class (℩𝑥 ∈ 𝐴 𝜑) |
5 | 2 | cv 1347 | . . . . 5 class 𝑥 |
6 | 5, 3 | wcel 2141 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 6, 1 | wa 103 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑) |
8 | 7, 2 | cio 5158 | . 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
9 | 4, 8 | wceq 1348 | 1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
Colors of variables: wff set class |
This definition is referenced by: riotaeqdv 5810 riotabidv 5811 riotaexg 5813 riotav 5814 riotauni 5815 nfriota1 5816 nfriotadxy 5817 cbvriota 5819 riotacl2 5822 riotabidva 5825 riota1 5827 riota2df 5829 snriota 5838 riotaund 5843 grpidvalg 12627 fn0g 12629 ismgmid 12631 bdcriota 13918 |
Copyright terms: Public domain | W3C validator |