Definition df-riota 7209

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 6373. (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 7208	. 2 class (℩𝑥 ∈ 𝐴 𝜑)
5	2	cv 1542	. . . . 5 class 𝑥
6	5, 3	wcel 2112	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 399	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cio 6371	. 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
9	4, 8	wceq 1543	1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  riotaeqdv  7210  riotabidv  7211  riotaex  7213  riotav  7214  riotauni  7215  nfriota1  7216  nfriotadw  7217  cbvriotaw  7218  cbvriotavw  7219  nfriotad  7221  cbvriota  7223  csbriota  7225  riotacl2  7226  riotabidva  7229  riota1  7231  riota2df  7233  snriota  7243  riotaund  7249  ismgmid  18239  q1peqb  25199  adjval  30128  riotarab  33550