Theorem riotaex

Description: Restricted iota is a set. (Contributed by NM, 15-Sep-2011)

	Ref	Expression
Assertion	riotaex	$$⊢\left(\iota x\in A|\psi \right)\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		df-riota	$$⊢\left(\iota x\in A|\psi \right)=\left(\iota x|\left(x\in A\wedge \psi \right)\right)$$
2		iotaex	$$⊢\left(\iota x|\left(x\in A\wedge \psi \right)\right)\in \mathrm{V}$$
3	1 2	eqeltri	$$⊢\left(\iota x\in A|\psi \right)\in \mathrm{V}$$