Definition df-riota 7306

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

This definition is referenced by:  riotaeqdv  7307  riotabidv  7308  riotaex  7310  riotav  7311  riotauni  7312  nfriota1  7313  nfriotadw  7314  cbvriotaw  7315  cbvriotavw  7316  nfriotad  7317  cbvriota  7319  csbriota  7321  riotacl2  7322  riotabidva  7325  riota1  7327  riota2df  7329  snriota  7339  riotaund  7345  riotarab  7348  ismgmid  18539  q1peqb  26059  adjval  31838  riotaeqbii  36192  cbvriotavw2  36230  cbvriotadavw  36264  cbvriotadavw2  36284