Definition df-riota 5738

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 5096. (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 5737	. 2 class (℩𝑥 ∈ 𝐴 𝜑)
5	2	cv 1331	. . . . 5 class 𝑥
6	5, 3	wcel 1481	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 103	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cio 5094	. 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
9	4, 8	wceq 1332	1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  riotaeqdv  5739  riotabidv  5740  riotaexg  5742  riotav  5743  riotauni  5744  nfriota1  5745  nfriotadxy  5746  cbvriota  5748  riotacl2  5751  riotabidva  5754  riota1  5756  riota2df  5758  snriota  5767  riotaund  5772  bdcriota  13252