![]() |
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 6501. (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 7374 | . 2 class (℩𝑥 ∈ 𝐴 𝜑) |
5 | 2 | cv 1532 | . . . . 5 class 𝑥 |
6 | 5, 3 | wcel 2098 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 6, 1 | wa 394 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑) |
8 | 7, 2 | cio 6499 | . 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
9 | 4, 8 | wceq 1533 | 1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
Colors of variables: wff setvar class |
This definition is referenced by: riotaeqdv 7376 riotabidv 7377 riotaex 7379 riotav 7380 riotauni 7381 nfriota1 7382 nfriotadw 7383 cbvriotaw 7384 cbvriotavw 7385 nfriotad 7387 cbvriota 7389 csbriota 7391 riotacl2 7392 riotabidva 7395 riota1 7397 riota2df 7399 snriota 7409 riotaund 7415 riotarab 7418 ismgmid 18628 q1peqb 26136 adjval 31772 |
Copyright terms: Public domain | W3C validator |