Definition df-riota 7365

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 6483. (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 7364	. 2 class (℩𝑥 ∈ 𝐴 𝜑)
5	2	cv 1569	. . . . 5 class 𝑥
6	5, 3	wcel 2145	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 401	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cio 6481	. 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
9	4, 8	wceq 1570	1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is used by:  riotaeqdv  7366  riotabidv  7367  riotaex  7369  riotav  7370  riotauni  7371  nfriota1  7372  nfriotadw  7373  cbvriotaw  7374  cbvriotavw  7375  nfriotad  7376  cbvriota  7378  csbriota  7380  riotacl2  7381  riotabidva  7384  riota1  7386  riota2df  7388  snriota  7398  riotaund  7404  riotarab  7407  idvalriota  18802  ismgmid  18806  q1peqb  26435  adjval  32425  riotaeqbii  36909  cbvriotavw2  36947  cbvriotadavw  36981  cbvriotadavw2  37001