Definition df-riota 5798

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 5153. (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 5797	. 2 class ( iota_ x e. A ph )
5	2	cv 1342	. . . . 5 class x
6	5, 3	wcel 2136	. . . 4 wff x e. A
7	6, 1	wa 103	. . 3 wff ( x e. A /\ ph )
8	7, 2	cio 5151	. 2 class ( iota x ( x e. A /\ ph ) )
9	4, 8	wceq 1343	1 wff ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )

This definition is referenced by:  riotaeqdv  5799  riotabidv  5800  riotaexg  5802  riotav  5803  riotauni  5804  nfriota1  5805  nfriotadxy  5806  cbvriota  5808  riotacl2  5811  riotabidva  5814  riota1  5816  riota2df  5818  snriota  5827  riotaund  5832  grpidvalg  12604  fn0g  12606  ismgmid  12608  bdcriota  13775