| 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 6514. (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 7387 | . 2 class (℩𝑥 ∈ 𝐴 𝜑) |
| 5 | 2 | cv 1539 | . . . . 5 class 𝑥 |
| 6 | 5, 3 | wcel 2108 | . . . 4 wff 𝑥 ∈ 𝐴 |
| 7 | 6, 1 | wa 395 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑) |
| 8 | 7, 2 | cio 6512 | . 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
| 9 | 4, 8 | wceq 1540 | 1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
| Colors of variables: wff setvar class |
| This definition is referenced by: riotaeqdv 7389 riotabidv 7390 riotaex 7392 riotav 7393 riotauni 7394 nfriota1 7395 nfriotadw 7396 cbvriotaw 7397 cbvriotavw 7398 nfriotad 7399 cbvriota 7401 csbriota 7403 riotacl2 7404 riotabidva 7407 riota1 7409 riota2df 7411 snriota 7421 riotaund 7427 riotarab 7430 ismgmid 18678 q1peqb 26195 adjval 31909 riotaeqbii 36199 cbvriotavw2 36237 cbvriotadavw 36271 cbvriotadavw2 36291 |
| Copyright terms: Public domain | W3C validator |