Definition df-riota 5833

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 5180. (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 5832	. 2 class ( iota_ x e. A ph )
5	2	cv 1352	. . . . 5 class x
6	5, 3	wcel 2148	. . . 4 wff x e. A
7	6, 1	wa 104	. . 3 wff ( x e. A /\ ph )
8	7, 2	cio 5178	. 2 class ( iota x ( x e. A /\ ph ) )
9	4, 8	wceq 1353	1 wff ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )

This definition is referenced by:  riotaeqdv  5834  riotabidv  5835  riotaexg  5837  riotav  5838  riotauni  5839  nfriota1  5840  nfriotadxy  5841  cbvriota  5843  riotacl2  5846  riotabidva  5849  riota1  5851  riota2df  5853  snriota  5862  riotaund  5867  grpidvalg  12797  fn0g  12799  ismgmid  12801  oppr1g  13257  bdcriota  14674