Definition df-riota 5411

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 4810. (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) = ( iotax(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 5410	. 2 class ( iota_x e. A ph)
5	2	cv 1241	. . . . 5 class x
6	5, 3	wcel 1390	. . . 4 wff x e. A
7	6, 1	wa 97	. . 3 wff (x e. A /\ ph)
8	7, 2	cio 4808	. 2 class ( iotax(x e. A /\ ph))
9	4, 8	wceq 1242	1 wff ( iota_x e. A ph) = ( iotax(x e. A /\ ph))

This definition is referenced by:  riotaeqdv  5412  riotabidv  5413  riotaexg  5415  riotav  5416  riotauni  5417  nfriota1  5418  nfriotadxy  5419  cbvriota  5421  riotacl2  5424  riotabidva  5427  riota1  5429  riota2df  5431  snriota  5440  riotaund  5445  bdcriota  9338