Definition df-riota 7225

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 6388. (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 7224	. 2 class (℩𝑥 ∈ 𝐴 𝜑)
5	2	cv 1540	. . . . 5 class 𝑥
6	5, 3	wcel 2109	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cio 6386	. 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
9	4, 8	wceq 1541	1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  riotaeqdv  7226  riotabidv  7227  riotaex  7229  riotav  7230  riotauni  7231  nfriota1  7232  nfriotadw  7233  cbvriotaw  7234  cbvriotavw  7235  nfriotad  7237  cbvriota  7239  csbriota  7241  riotacl2  7242  riotabidva  7245  riota1  7247  riota2df  7249  snriota  7259  riotaund  7265  ismgmid  18330  q1peqb  25300  adjval  30231  riotarab  33652