Definition df-riota 7321

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

This definition is referenced by:  riotaeqdv  7322  riotabidv  7323  riotaex  7325  riotav  7326  riotauni  7327  nfriota1  7328  nfriotadw  7329  cbvriotaw  7330  cbvriotavw  7331  nfriotad  7332  cbvriota  7334  csbriota  7336  riotacl2  7337  riotabidva  7340  riota1  7342  riota2df  7344  snriota  7354  riotaund  7360  riotarab  7363  ismgmid  18630  q1peqb  26118  adjval  31958  riotaeqbii  36377  cbvriotavw2  36415  cbvriotadavw  36449  cbvriotadavw2  36469