Definition df-riota 7397

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 6509. (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 7396	. 2 class (℩𝑥 ∈ 𝐴 𝜑)
5	2	cv 1569	. . . . 5 class 𝑥
6	5, 3	wcel 2147	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 401	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cio 6507	. 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
9	4, 8	wceq 1570	1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is used by:  riotaeqdv  7398  riotabidv  7399  riotaex  7401  riotav  7402  riotauni  7403  nfriota1  7404  nfriotadw  7405  cbvriotaw  7406  cbvriotavw  7407  nfriotad  7408  cbvriota  7410  csbriota  7412  riotacl2  7413  riotabidva  7416  riota1  7418  riota2df  7420  snriota  7430  riotaund  7436  riotarab  7439  idvalriota  18867  ismgmid  18871  q1peqb  26501  adjval  32519  riotaeqbii  37164  cbvriotavw2  37202  cbvriotadavw  37236  cbvriotadavw2  37256