Definition df-riota 5662

Description: Define restricted description binder. In case there is no unique x such that ( x e. A /\ ph ) holds, it evaluates to the empty set. See also comments for df-iota 5024. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) (Revised by NM, 2-Sep-2018.)

Assertion

Ref	Expression
df-riota	|- ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )

Detailed syntax breakdown of Definition df-riota

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		vx	. . 3 setvar x
3		cA	. . 3 class A
4	1, 2, 3	crio 5661	. 2 class ( iota_ x e. A ph )
5	2	cv 1298	. . . . 5 class x
6	5, 3	wcel 1448	. . . 4 wff x e. A
7	6, 1	wa 103	. . 3 wff ( x e. A /\ ph )
8	7, 2	cio 5022	. 2 class ( iota x ( x e. A /\ ph ) )
9	4, 8	wceq 1299	1 wff ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )

This definition is referenced by:  riotaeqdv  5663  riotabidv  5664  riotaexg  5666  riotav  5667  riotauni  5668  nfriota1  5669  nfriotadxy  5670  cbvriota  5672  riotacl2  5675  riotabidva  5678  riota1  5680  riota2df  5682  snriota  5691  riotaund  5696  bdcriota  12662