Definition df-riota 7388

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 6514. (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 7387	. 2 class (℩𝑥 ∈ 𝐴 𝜑)
5	2	cv 1539	. . . . 5 class 𝑥
6	5, 3	wcel 2108	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cio 6512	. 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
9	4, 8	wceq 1540	1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  riotaeqdv  7389  riotabidv  7390  riotaex  7392  riotav  7393  riotauni  7394  nfriota1  7395  nfriotadw  7396  cbvriotaw  7397  cbvriotavw  7398  nfriotad  7399  cbvriota  7401  csbriota  7403  riotacl2  7404  riotabidva  7407  riota1  7409  riota2df  7411  snriota  7421  riotaund  7427  riotarab  7430  ismgmid  18678  q1peqb  26195  adjval  31909  riotaeqbii  36199  cbvriotavw2  36237  cbvriotadavw  36271  cbvriotadavw2  36291