Definition df-riota 7355

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 6479. (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 7354	. 2 class (℩𝑥 ∈ 𝐴 𝜑)
5	2	cv 1561	. . . . 5 class 𝑥
6	5, 3	wcel 2144	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 399	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cio 6477	. 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
9	4, 8	wceq 1562	1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  riotaeqdv  7356  riotabidv  7357  riotaex  7359  riotav  7360  riotauni  7361  nfriota1  7362  nfriotadw  7363  cbvriotaw  7364  cbvriotavw  7365  nfriotad  7366  cbvriota  7368  csbriota  7370  riotacl2  7371  riotabidva  7374  riota1  7376  riota2df  7378  snriota  7388  riotaund  7394  riotarab  7397  ismgmid  18701  q1peqb  26218  adjval  32095  riotaeqbii  36563  cbvriotavw2  36601  cbvriotadavw  36635  cbvriotadavw2  36655