Definition df-riota 6005

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 5314. (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 6004	. 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 5312	. 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
9	4, 8	wceq 1398	1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  riotaeqdv  6006  riotabidv  6007  riotaexg  6009  iotaexel  6010  riotav  6011  riotauni  6012  nfriota1  6013  nfriotadxy  6014  cbvriotavw  6016  cbvriota  6017  riotacl2  6020  riotabidva  6023  riota1  6025  riota2df  6027  snriota  6037  riotaund  6042  grpidvalg  13603  fn0g  13605  ismgmid  13607  oppr1g  14243  bdcriota  16670