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 6308. (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 7102 | . 2 class (℩𝑥 ∈ 𝐴 𝜑) |
5 | 2 | cv 1527 | . . . . 5 class 𝑥 |
6 | 5, 3 | wcel 2105 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 6, 1 | wa 396 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑) |
8 | 7, 2 | cio 6306 | . 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
9 | 4, 8 | wceq 1528 | 1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
Colors of variables: wff setvar class |
This definition is referenced by: riotaeqdv 7104 riotabidv 7105 riotaex 7107 riotav 7108 riotauni 7109 nfriota1 7110 nfriotadw 7111 cbvriotaw 7112 nfriotad 7114 cbvriota 7116 csbriota 7118 riotacl2 7119 riotabidva 7122 riota1 7124 riota2df 7126 snriota 7136 riotaund 7142 ismgmid 17865 q1peqb 24677 adjval 29595 |
Copyright terms: Public domain | W3C validator |