Definition df-riota 7309

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 6443. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) (Revised by NM, 2-Sep-2018.)

Assertion

Ref	Expression
df-riota	⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

Detailed syntax breakdown of Definition df-riota

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3		cA	. . 3 class 𝐴
4	1, 2, 3	crio 7308	. 2 class (℩𝑥 ∈ 𝐴 𝜑)
5	2	cv 1540	. . . . 5 class 𝑥
6	5, 3	wcel 2111	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cio 6441	. 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
9	4, 8	wceq 1541	1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  riotaeqdv  7310  riotabidv  7311  riotaex  7313  riotav  7314  riotauni  7315  nfriota1  7316  nfriotadw  7317  cbvriotaw  7318  cbvriotavw  7319  nfriotad  7320  cbvriota  7322  csbriota  7324  riotacl2  7325  riotabidva  7328  riota1  7330  riota2df  7332  snriota  7342  riotaund  7348  riotarab  7351  ismgmid  18579  q1peqb  26094  adjval  31877  riotaeqbii  36249  cbvriotavw2  36287  cbvriotadavw  36321  cbvriotadavw2  36341