Definition df-riota 5994

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 5303. (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 5993	. 2 class ( iota_ x e. A ph )
5	2	cv 1397	. . . . 5 class x
6	5, 3	wcel 2203	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	cio 5301	. 2 class ( iota x ( x e. A /\ ph ) )
9	4, 8	wceq 1398	1 wff ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )

This definition is referenced by:  riotaeqdv  5995  riotabidv  5996  riotaexg  5998  iotaexel  5999  riotav  6000  riotauni  6001  nfriota1  6002  nfriotadxy  6003  cbvriotavw  6005  cbvriota  6006  riotacl2  6009  riotabidva  6012  riota1  6014  riota2df  6016  snriota  6026  riotaund  6031  grpidvalg  13560  fn0g  13562  ismgmid  13564  oppr1g  14200  bdcriota  16623