Definition df-riota 7326

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

This definition is referenced by:  riotaeqdv  7327  riotabidv  7328  riotaex  7330  riotav  7331  riotauni  7332  nfriota1  7333  nfriotadw  7334  cbvriotaw  7335  cbvriotavw  7336  nfriotad  7337  cbvriota  7339  csbriota  7341  riotacl2  7342  riotabidva  7345  riota1  7347  riota2df  7349  snriota  7359  riotaund  7365  riotarab  7368  ismgmid  18574  q1peqb  26094  adjval  31869  riotaeqbii  36179  cbvriotavw2  36217  cbvriotadavw  36251  cbvriotadavw2  36271