Definition df-riota 5880

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 5220. (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 5879	. 2 class ( iota_ x e. A ph )
5	2	cv 1363	. . . . 5 class x
6	5, 3	wcel 2167	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	cio 5218	. 2 class ( iota x ( x e. A /\ ph ) )
9	4, 8	wceq 1364	1 wff ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )

This definition is referenced by:  riotaeqdv  5881  riotabidv  5882  riotaexg  5884  iotaexel  5885  riotav  5886  riotauni  5887  nfriota1  5888  nfriotadxy  5889  cbvriota  5891  riotacl2  5894  riotabidva  5897  riota1  5899  riota2df  5901  snriota  5910  riotaund  5915  grpidvalg  13075  fn0g  13077  ismgmid  13079  oppr1g  13714  bdcriota  15613