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 6494. (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 1538	. . . . 5 class 𝑥
6	5, 3	wcel 2104	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 394	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cio 6492	. 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
9	4, 8	wceq 1539	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  7379  cbvriota  7381  csbriota  7383  riotacl2  7384  riotabidva  7387  riota1  7389  riota2df  7391  snriota  7401  riotaund  7407  riotarab  7410  ismgmid  18590  q1peqb  25907  adjval  31410