Definition df-riota 7318

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 6449. (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 7317	. 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 6447	. 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
9	4, 8	wceq 1542	1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  riotaeqdv  7319  riotabidv  7320  riotaex  7322  riotav  7323  riotauni  7324  nfriota1  7325  nfriotadw  7326  cbvriotaw  7327  cbvriotavw  7328  nfriotad  7329  cbvriota  7331  csbriota  7333  riotacl2  7334  riotabidva  7337  riota1  7339  riota2df  7341  snriota  7351  riotaund  7357  riotarab  7360  ismgmid  18595  q1peqb  26122  adjval  31970  riotaeqbii  36405  cbvriotavw2  36443  cbvriotadavw  36477  cbvriotadavw2  36497