Definition df-riota 6011

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 5317. (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 6010	. 2 class (℩𝑥 ∈ 𝐴 𝜑)
5	2	cv 1397	. . . . 5 class 𝑥
6	5, 3	wcel 2205	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 104	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cio 5315	. 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
9	4, 8	wceq 1398	1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  riotaeqdv  6012  riotabidv  6013  riotaexg  6015  iotaexel  6016  riotav  6017  riotauni  6018  nfriota1  6019  nfriotadxy  6020  cbvriotavw  6022  cbvriota  6023  riotacl2  6026  riotabidva  6029  riota1  6031  riota2df  6033  snriota  6043  riotaund  6048  grpidvalg  13636  fn0g  13638  ismgmid  13640  oppr1g  14326  bdcriota  16779