Definition df-riota 7373

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

This definition is used by:  riotaeqdv  7374  riotabidv  7375  riotaex  7377  riotav  7378  riotauni  7379  nfriota1  7380  nfriotadw  7381  cbvriotaw  7382  cbvriotavw  7383  nfriotad  7384  cbvriota  7386  csbriota  7388  riotacl2  7389  riotabidva  7392  riota1  7394  riota2df  7396  snriota  7406  riotaund  7412  riotarab  7415  ismgmid  18762  q1peqb  26383  adjval  32357  riotaeqbii  36805  cbvriotavw2  36843  cbvriotadavw  36877  cbvriotadavw2  36897