Definition df-riota

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 . (Contributed by NM, 15-Sep-2011) (Revised by Mario Carneiro, 15-Oct-2016) (Revised by NM, 2-Sep-2018)

	Ref	Expression
Assertion	df-riota	|- ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	|- x
1		cA	|- A
2		wph	|- ph
3	2 0 1	crio	|- ( iota_ x e. A ph )
4	0	cv	|- x
5	4 1	wcel	|- x e. A
6	5 2	wa	|- ( x e. A /\ ph )
7	6 0	cio	|- ( iota x ( x e. A /\ ph ) )
8	3 7	wceq	|- ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )