Definition df-riota 5874

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 5216. (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 5873	. 2 class (℩𝑥 ∈ 𝐴 𝜑)
5	2	cv 1363	. . . . 5 class 𝑥
6	5, 3	wcel 2164	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 104	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cio 5214	. 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
9	4, 8	wceq 1364	1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  riotaeqdv  5875  riotabidv  5876  riotaexg  5878  iotaexel  5879  riotav  5880  riotauni  5881  nfriota1  5882  nfriotadxy  5883  cbvriota  5885  riotacl2  5888  riotabidva  5891  riota1  5893  riota2df  5895  snriota  5904  riotaund  5909  grpidvalg  12959  fn0g  12961  ismgmid  12963  oppr1g  13581  bdcriota  15445