Definition df-riota 7360

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 7359	. 2 class (℩𝑥 ∈ 𝐴 𝜑)
5	2	cv 1539	. . . . 5 class 𝑥
6	5, 3	wcel 2108	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cio 6481	. 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
9	4, 8	wceq 1540	1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  riotaeqdv  7361  riotabidv  7362  riotaex  7364  riotav  7365  riotauni  7366  nfriota1  7367  nfriotadw  7368  cbvriotaw  7369  cbvriotavw  7370  nfriotad  7371  cbvriota  7373  csbriota  7375  riotacl2  7376  riotabidva  7379  riota1  7381  riota2df  7383  snriota  7393  riotaund  7399  riotarab  7402  ismgmid  18641  q1peqb  26111  adjval  31817  riotaeqbii  36162  cbvriotavw2  36200  cbvriotadavw  36234  cbvriotadavw2  36254