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 5768. (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 6510 | . 2 class (℩𝑥 ∈ 𝐴 𝜑) |
5 | 2 | cv 1474 | . . . . 5 class 𝑥 |
6 | 5, 3 | wcel 1977 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 6, 1 | wa 383 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑) |
8 | 7, 2 | cio 5766 | . 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
9 | 4, 8 | wceq 1475 | 1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
Colors of variables: wff setvar class |
This definition is referenced by: riotaeqdv 6512 riotabidv 6513 riotaex 6515 riotav 6516 riotauni 6517 nfriota1 6518 nfriotad 6519 cbvriota 6521 csbriota 6523 riotacl2 6524 riotabidva 6527 riota1 6529 riota2df 6531 snriota 6540 riotaund 6546 ismgmid 17087 q1peqb 23718 adjval 28133 |
Copyright terms: Public domain | W3C validator |