Definition df-riota 7369

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

This definition is used by:  riotaeqdv  7370  riotabidv  7371  riotaex  7373  riotav  7374  riotauni  7375  nfriota1  7376  nfriotadw  7377  cbvriotaw  7378  cbvriotavw  7379  nfriotad  7380  cbvriota  7382  csbriota  7384  riotacl2  7385  riotabidva  7388  riota1  7390  riota2df  7392  snriota  7402  riotaund  7408  riotarab  7411  ismgmid  18729  q1peqb  26324  adjval  32253  riotaeqbii  36738  cbvriotavw2  36776  cbvriotadavw  36810  cbvriotadavw2  36830