Definition df-riota 7114

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 6314. (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 7113	. 2 class (℩𝑥 ∈ 𝐴 𝜑)
5	2	cv 1536	. . . . 5 class 𝑥
6	5, 3	wcel 2114	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 398	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cio 6312	. 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
9	4, 8	wceq 1537	1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  riotaeqdv  7115  riotabidv  7116  riotaex  7118  riotav  7119  riotauni  7120  nfriota1  7121  nfriotadw  7122  cbvriotaw  7123  nfriotad  7125  cbvriota  7127  csbriota  7129  riotacl2  7130  riotabidva  7133  riota1  7135  riota2df  7137  snriota  7147  riotaund  7153  ismgmid  17875  q1peqb  24748  adjval  29667