Definition df-riota 6831

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 6060. (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 6830	. 2 class (℩𝑥 ∈ 𝐴 𝜑)
5	2	cv 1636	. . . . 5 class 𝑥
6	5, 3	wcel 2156	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 384	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cio 6058	. 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
9	4, 8	wceq 1637	1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  riotaeqdv  6832  riotabidv  6833  riotaex  6835  riotav  6836  riotauni  6837  nfriota1  6838  nfriotad  6839  cbvriota  6841  csbriota  6843  riotacl2  6844  riotabidva  6847  riota1  6849  riota2df  6851  snriota  6861  riotaund  6867  ismgmid  17465  q1peqb  24124  adjval  29073