Definition df-riota 7404

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 6525. (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 7403	. 2 class (℩𝑥 ∈ 𝐴 𝜑)
5	2	cv 1536	. . . . 5 class 𝑥
6	5, 3	wcel 2108	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cio 6523	. 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
9	4, 8	wceq 1537	1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  riotaeqdv  7405  riotabidv  7406  riotaex  7408  riotav  7409  riotauni  7410  nfriota1  7411  nfriotadw  7412  cbvriotaw  7413  cbvriotavw  7414  nfriotad  7416  cbvriota  7418  csbriota  7420  riotacl2  7421  riotabidva  7424  riota1  7426  riota2df  7428  snriota  7438  riotaund  7444  riotarab  7447  ismgmid  18703  q1peqb  26215  adjval  31922  riotaeqbii  36162  cbvriotavw2  36202  cbvriotadavw  36236  cbvriotadavw2  36256