Definition df-riota 7313

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 6443. (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 7312	. 2 class (℩𝑥 ∈ 𝐴 𝜑)
5	2	cv 1541	. . . . 5 class 𝑥
6	5, 3	wcel 2114	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cio 6441	. 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
9	4, 8	wceq 1542	1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  riotaeqdv  7314  riotabidv  7315  riotaex  7317  riotav  7318  riotauni  7319  nfriota1  7320  nfriotadw  7321  cbvriotaw  7322  cbvriotavw  7323  nfriotad  7324  cbvriota  7326  csbriota  7328  riotacl2  7329  riotabidva  7332  riota1  7334  riota2df  7336  snriota  7346  riotaund  7352  riotarab  7355  ismgmid  18622  q1peqb  26109  adjval  31949  riotaeqbii  36368  cbvriotavw2  36406  cbvriotadavw  36440  cbvriotadavw2  36460