Definition df-riota 6038

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 5337. (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 6037	. 2 class (℩𝑥 ∈ 𝐴 𝜑)
5	2	cv 1401	. . . . 5 class 𝑥
6	5, 3	wcel 2209	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 104	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cio 5335	. 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
9	4, 8	wceq 1402	1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is used by:  riotaeqdv  6039  riotabidv  6040  riotaexg  6042  iotaexel  6043  riotav  6044  riotauni  6045  nfriota1  6046  nfriotadxy  6047  cbvriotavw  6049  cbvriota  6050  riotacl2  6053  riotabidva  6056  riota1  6058  riota2df  6060  snriota  6070  riotaund  6075  grpidvalg  13693  fn0g  13695  ismgmid  13697  oppr1g  14388  bdcriota  16909