Definition df-riota 7387

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 6515. (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 7386	. 2 class (℩𝑥 ∈ 𝐴 𝜑)
5	2	cv 1535	. . . . 5 class 𝑥
6	5, 3	wcel 2105	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cio 6513	. 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
9	4, 8	wceq 1536	1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  riotaeqdv  7388  riotabidv  7389  riotaex  7391  riotav  7392  riotauni  7393  nfriota1  7394  nfriotadw  7395  cbvriotaw  7396  cbvriotavw  7397  nfriotad  7398  cbvriota  7400  csbriota  7402  riotacl2  7403  riotabidva  7406  riota1  7408  riota2df  7410  snriota  7420  riotaund  7426  riotarab  7429  ismgmid  18690  q1peqb  26209  adjval  31918  riotaeqbii  36179  cbvriotavw2  36218  cbvriotadavw  36252  cbvriotadavw2  36272