Definition df-riota 5901

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 5233. (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 5900	. 2 class ( iota_ x e. A ph )
5	2	cv 1372	. . . . 5 class x
6	5, 3	wcel 2176	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	cio 5231	. 2 class ( iota x ( x e. A /\ ph ) )
9	4, 8	wceq 1373	1 wff ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )

This definition is referenced by:  riotaeqdv  5902  riotabidv  5903  riotaexg  5905  iotaexel  5906  riotav  5907  riotauni  5908  nfriota1  5909  nfriotadxy  5910  cbvriota  5912  riotacl2  5915  riotabidva  5918  riota1  5920  riota2df  5922  snriota  5931  riotaund  5936  grpidvalg  13238  fn0g  13240  ismgmid  13242  oppr1g  13877  bdcriota  15856