Definition df-riota 5873

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 5215. (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 5872	. 2 class ( iota_ x e. A ph )
5	2	cv 1363	. . . . 5 class x
6	5, 3	wcel 2164	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	cio 5213	. 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  5874  riotabidv  5875  riotaexg  5877  iotaexel  5878  riotav  5879  riotauni  5880  nfriota1  5881  nfriotadxy  5882  cbvriota  5884  riotacl2  5887  riotabidva  5890  riota1  5892  riota2df  5894  snriota  5903  riotaund  5908  grpidvalg  12956  fn0g  12958  ismgmid  12960  oppr1g  13578  bdcriota  15375