Definition df-riota 5806

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 5158. (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 5805	. 2 class ( iota_ x e. A ph )
5	2	cv 1347	. . . . 5 class x
6	5, 3	wcel 2141	. . . 4 wff x e. A
7	6, 1	wa 103	. . 3 wff ( x e. A /\ ph )
8	7, 2	cio 5156	. 2 class ( iota x ( x e. A /\ ph ) )
9	4, 8	wceq 1348	1 wff ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )

This definition is referenced by:  riotaeqdv  5807  riotabidv  5808  riotaexg  5810  riotav  5811  riotauni  5812  nfriota1  5813  nfriotadxy  5814  cbvriota  5816  riotacl2  5819  riotabidva  5822  riota1  5824  riota2df  5826  snriota  5835  riotaund  5840  grpidvalg  12614  fn0g  12616  ismgmid  12618  bdcriota  13878