Definition df-riota 5844

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 5190. (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 5843	. 2 class ( iota_ x e. A ph )
5	2	cv 1362	. . . . 5 class x
6	5, 3	wcel 2158	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	cio 5188	. 2 class ( iota x ( x e. A /\ ph ) )
9	4, 8	wceq 1363	1 wff ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )

This definition is referenced by:  riotaeqdv  5845  riotabidv  5846  riotaexg  5848  riotav  5849  riotauni  5850  nfriota1  5851  nfriotadxy  5852  cbvriota  5854  riotacl2  5857  riotabidva  5860  riota1  5862  riota2df  5864  snriota  5873  riotaund  5878  grpidvalg  12811  fn0g  12813  ismgmid  12815  oppr1g  13330  bdcriota  14931