Definition df-riota 5877

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

This definition is referenced by:  riotaeqdv  5878  riotabidv  5879  riotaexg  5881  iotaexel  5882  riotav  5883  riotauni  5884  nfriota1  5885  nfriotadxy  5886  cbvriota  5888  riotacl2  5891  riotabidva  5894  riota1  5896  riota2df  5898  snriota  5907  riotaund  5912  grpidvalg  13016  fn0g  13018  ismgmid  13020  oppr1g  13638  bdcriota  15529