Definition df-riota 6651

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 5889. (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 6650	. 2 class (℩𝑥 ∈ 𝐴 𝜑)
5	2	cv 1522	. . . . 5 class 𝑥
6	5, 3	wcel 2030	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 383	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cio 5887	. 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
9	4, 8	wceq 1523	1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  riotaeqdv  6652  riotabidv  6653  riotaex  6655  riotav  6656  riotauni  6657  nfriota1  6658  nfriotad  6659  cbvriota  6661  csbriota  6663  riotacl2  6664  riotabidva  6667  riota1  6669  riota2df  6671  snriota  6681  riotaund  6687  ismgmid  17311  q1peqb  23959  adjval  28877