Definition df-riota 7377

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 6494. (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 7376	. 2 class (℩𝑥 ∈ 𝐴 𝜑)
5	2	cv 1568	. . . . 5 class 𝑥
6	5, 3	wcel 2144	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 401	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cio 6492	. 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
9	4, 8	wceq 1569	1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is used by:  riotaeqdv  7378  riotabidv  7379  riotaex  7381  riotav  7382  riotauni  7383  nfriota1  7384  nfriotadw  7385  cbvriotaw  7386  cbvriotavw  7387  nfriotad  7388  cbvriota  7390  csbriota  7392  riotacl2  7393  riotabidva  7396  riota1  7398  riota2df  7400  snriota  7410  riotaund  7416  riotarab  7419  idvalriota  18841  ismgmid  18845  q1peqb  26474  adjval  32492  riotaeqbii  37029  cbvriotavw2  37067  cbvriotadavw  37101  cbvriotadavw2  37121