Definition df-riota 5960

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 5278. (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 5959	. 2 class (℩𝑥 ∈ 𝐴 𝜑)
5	2	cv 1394	. . . . 5 class 𝑥
6	5, 3	wcel 2200	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wa 104	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑)
8	7, 2	cio 5276	. 2 class (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
9	4, 8	wceq 1395	1 wff (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))

This definition is referenced by:  riotaeqdv  5961  riotabidv  5962  riotaexg  5964  iotaexel  5965  riotav  5966  riotauni  5967  nfriota1  5968  nfriotadxy  5969  cbvriotavw  5971  cbvriota  5972  riotacl2  5975  riotabidva  5978  riota1  5980  riota2df  5982  snriota  5992  riotaund  5997  grpidvalg  13422  fn0g  13424  ismgmid  13426  oppr1g  14061  bdcriota  16329