Definition df-riota 6937

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 6152. (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 6936	. 2 class (℩𝑥 ∈ 𝐴 𝜑)
5	2	cv 1506	. . . . 5 class 𝑥
6	5, 3	wcel 2050	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 387	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cio 6150	. 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
9	4, 8	wceq 1507	1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  riotaeqdv  6938  riotabidv  6939  riotaex  6941  riotav  6942  riotauni  6943  nfriota1  6944  nfriotad  6945  cbvriota  6947  csbriota  6949  riotacl2  6950  riotabidva  6953  riota1  6955  riota2df  6957  snriota  6967  riotaund  6973  ismgmid  17732  q1peqb  24451  adjval  29448