![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-riota | Structured version Visualization version 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 6152. (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 6936 | . 2 class (℩𝑥 ∈ 𝐴 𝜑) |
5 | 2 | cv 1506 | . . . . 5 class 𝑥 |
6 | 5, 3 | wcel 2050 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 6, 1 | wa 387 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑) |
8 | 7, 2 | cio 6150 | . 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
9 | 4, 8 | wceq 1507 | 1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
Colors of variables: wff setvar class |
This definition is referenced by: riotaeqdv 6938 riotabidv 6939 riotaex 6941 riotav 6942 riotauni 6943 nfriota1 6944 nfriotad 6945 cbvriota 6947 csbriota 6949 riotacl2 6950 riotabidva 6953 riota1 6955 riota2df 6957 snriota 6967 riotaund 6973 ismgmid 17732 q1peqb 24451 adjval 29448 |
Copyright terms: Public domain | W3C validator |