Definition df-riota 7365

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

This definition is referenced by:  riotaeqdv  7366  riotabidv  7367  riotaex  7369  riotav  7370  riotauni  7371  nfriota1  7372  nfriotadw  7373  cbvriotaw  7374  cbvriotavw  7375  nfriotad  7377  cbvriota  7379  csbriota  7381  riotacl2  7382  riotabidva  7385  riota1  7387  riota2df  7389  snriota  7399  riotaund  7405  riotarab  7408  ismgmid  18584  q1peqb  25672  adjval  31143