Definition df-riota 5899

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 5232. (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 5898	. 2 class (℩𝑥 ∈ 𝐴 𝜑)
5	2	cv 1372	. . . . 5 class 𝑥
6	5, 3	wcel 2176	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 104	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cio 5230	. 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
9	4, 8	wceq 1373	1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  riotaeqdv  5900  riotabidv  5901  riotaexg  5903  iotaexel  5904  riotav  5905  riotauni  5906  nfriota1  5907  nfriotadxy  5908  cbvriota  5910  riotacl2  5913  riotabidva  5916  riota1  5918  riota2df  5920  snriota  5929  riotaund  5934  grpidvalg  13205  fn0g  13207  ismgmid  13209  oppr1g  13844  bdcriota  15823