Definition df-riota 5974

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 5286. (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 5973	. 2 class ( iota_ x e. A ph )
5	2	cv 1396	. . . . 5 class x
6	5, 3	wcel 2202	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	cio 5284	. 2 class ( iota x ( x e. A /\ ph ) )
9	4, 8	wceq 1397	1 wff ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )

This definition is referenced by:  riotaeqdv  5975  riotabidv  5976  riotaexg  5978  iotaexel  5979  riotav  5980  riotauni  5981  nfriota1  5982  nfriotadxy  5983  cbvriotavw  5985  cbvriota  5986  riotacl2  5989  riotabidva  5992  riota1  5994  riota2df  5996  snriota  6006  riotaund  6011  grpidvalg  13477  fn0g  13479  ismgmid  13481  oppr1g  14117  bdcriota  16537