![]() |
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 5179. (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 5830 | . 2 class (℩𝑥 ∈ 𝐴 𝜑) |
5 | 2 | cv 1352 | . . . . 5 class 𝑥 |
6 | 5, 3 | wcel 2148 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 6, 1 | wa 104 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑) |
8 | 7, 2 | cio 5177 | . 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
9 | 4, 8 | wceq 1353 | 1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
Colors of variables: wff set class |
This definition is referenced by: riotaeqdv 5832 riotabidv 5833 riotaexg 5835 riotav 5836 riotauni 5837 nfriota1 5838 nfriotadxy 5839 cbvriota 5841 riotacl2 5844 riotabidva 5847 riota1 5849 riota2df 5851 snriota 5860 riotaund 5865 grpidvalg 12792 fn0g 12794 ismgmid 12796 oppr1g 13252 bdcriota 14638 |
Copyright terms: Public domain | W3C validator |