Definition df-riota 7375

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 6501. (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 7374	. 2 class (℩𝑥 ∈ 𝐴 𝜑)
5	2	cv 1532	. . . . 5 class 𝑥
6	5, 3	wcel 2098	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 394	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cio 6499	. 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
9	4, 8	wceq 1533	1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  riotaeqdv  7376  riotabidv  7377  riotaex  7379  riotav  7380  riotauni  7381  nfriota1  7382  nfriotadw  7383  cbvriotaw  7384  cbvriotavw  7385  nfriotad  7387  cbvriota  7389  csbriota  7391  riotacl2  7392  riotabidva  7395  riota1  7397  riota2df  7399  snriota  7409  riotaund  7415  riotarab  7418  ismgmid  18628  q1peqb  26136  adjval  31772