Definition df-riota 7367

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 6492. (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 7366	. 2 class (℩𝑥 ∈ 𝐴 𝜑)
5	2	cv 1567	. . . . 5 class 𝑥
6	5, 3	wcel 2141	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 400	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cio 6490	. 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
9	4, 8	wceq 1568	1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  riotaeqdv  7368  riotabidv  7369  riotaex  7371  riotav  7372  riotauni  7373  nfriota1  7374  nfriotadw  7375  cbvriotaw  7376  cbvriotavw  7377  nfriotad  7378  cbvriota  7380  csbriota  7382  riotacl2  7383  riotabidva  7386  riota1  7388  riota2df  7390  snriota  7400  riotaund  7406  riotarab  7409  ismgmid  18722  q1peqb  26292  adjval  32208  riotaeqbii  36654  cbvriotavw2  36692  cbvriotadavw  36726  cbvriotadavw2  36746