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	$$⊢\left(\iota x\in A|\phi \right)=\left(\iota x|\left(x\in A\wedge \phi \right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		cA	$$classA$$
2		wph	$$wff\phi$$
3	2 0 1	crio	$$class\left(\iota x\in A|\phi \right)$$
4	0	cv	$$setvarx$$
5	4 1	wcel	$$wffx\in A$$
6	5 2	wa	$$wff\left(x\in A\wedge \phi \right)$$
7	6 0	cio	$$class\left(\iota x|\left(x\in A\wedge \phi \right)\right)$$
8	3 7	wceq	$$wff\left(\iota x\in A|\phi \right)=\left(\iota x|\left(x\in A\wedge \phi \right)\right)$$