![]() |
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 5178. (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 5829 | . 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 5176 | . 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
9 | 4, 8 | wceq 1353 | 1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
Colors of variables: wff set class |
This definition is referenced by: riotaeqdv 5831 riotabidv 5832 riotaexg 5834 riotav 5835 riotauni 5836 nfriota1 5837 nfriotadxy 5838 cbvriota 5840 riotacl2 5843 riotabidva 5846 riota1 5848 riota2df 5850 snriota 5859 riotaund 5864 grpidvalg 12791 fn0g 12793 ismgmid 12795 oppr1g 13250 bdcriota 14605 |
Copyright terms: Public domain | W3C validator |