Definition df-riota 7232

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 6391. (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 7231	. 2 class (℩𝑥 ∈ 𝐴 𝜑)
5	2	cv 1538	. . . . 5 class 𝑥
6	5, 3	wcel 2106	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 396	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cio 6389	. 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
9	4, 8	wceq 1539	1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  riotaeqdv  7233  riotabidv  7234  riotaex  7236  riotav  7237  riotauni  7238  nfriota1  7239  nfriotadw  7240  cbvriotaw  7241  cbvriotavw  7242  nfriotad  7244  cbvriota  7246  csbriota  7248  riotacl2  7249  riotabidva  7252  riota1  7254  riota2df  7256  snriota  7266  riotaund  7272  ismgmid  18349  q1peqb  25319  adjval  30252  riotarab  33673