Definition df-riota 6611

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 5851. (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 6610	. 2 class (℩𝑥 ∈ 𝐴 𝜑)
5	2	cv 1482	. . . . 5 class 𝑥
6	5, 3	wcel 1990	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 384	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cio 5849	. 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
9	4, 8	wceq 1483	1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  riotaeqdv  6612  riotabidv  6613  riotaex  6615  riotav  6616  riotauni  6617  nfriota1  6618  nfriotad  6619  cbvriota  6621  csbriota  6623  riotacl2  6624  riotabidva  6627  riota1  6629  riota2df  6631  snriota  6641  riotaund  6647  ismgmid  17264  q1peqb  23914  adjval  28749