Definition df-riota 7344

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

This definition is referenced by:  riotaeqdv  7345  riotabidv  7346  riotaex  7348  riotav  7349  riotauni  7350  nfriota1  7351  nfriotadw  7352  cbvriotaw  7353  cbvriotavw  7354  nfriotad  7355  cbvriota  7357  csbriota  7359  riotacl2  7360  riotabidva  7363  riota1  7365  riota2df  7367  snriota  7377  riotaund  7383  riotarab  7386  ismgmid  18592  q1peqb  26061  adjval  31819  riotaeqbii  36186  cbvriotavw2  36224  cbvriotadavw  36258  cbvriotadavw2  36278