Definition df-riota 5922

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 5251. (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 5921	. 2 class (℩𝑥 ∈ 𝐴 𝜑)
5	2	cv 1372	. . . . 5 class 𝑥
6	5, 3	wcel 2178	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 104	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cio 5249	. 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
9	4, 8	wceq 1373	1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  riotaeqdv  5923  riotabidv  5924  riotaexg  5926  iotaexel  5927  riotav  5928  riotauni  5929  nfriota1  5930  nfriotadxy  5931  cbvriota  5933  riotacl2  5936  riotabidva  5939  riota1  5941  riota2df  5943  snriota  5952  riotaund  5957  grpidvalg  13320  fn0g  13322  ismgmid  13324  oppr1g  13959  bdcriota  16018