Definition df-riota 7316

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 6444. (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 7315	. 2 class (℩𝑥 ∈ 𝐴 𝜑)
5	2	cv 1547	. . . . 5 class 𝑥
6	5, 3	wcel 2121	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 397	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cio 6442	. 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
9	4, 8	wceq 1548	1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  riotaeqdv  7317  riotabidv  7318  riotaex  7320  riotav  7321  riotauni  7322  nfriota1  7323  nfriotadw  7324  cbvriotaw  7325  cbvriotavw  7326  nfriotad  7327  cbvriota  7329  csbriota  7331  riotacl2  7332  riotabidva  7335  riota1  7337  riota2df  7339  snriota  7349  riotaund  7355  riotarab  7358  ismgmid  18628  q1peqb  26142  adjval  31981  riotaeqbii  36439  cbvriotavw2  36477  cbvriotadavw  36511  cbvriotadavw2  36531