Theorem riotaex

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

	Ref	Expression
Assertion	riotaex	|- ( iota_ x e. A ps ) e. _V

Proof

Step	Hyp	Ref	Expression
1		df-riota	|- ( iota_ x e. A ps ) = ( iota x ( x e. A /\ ps ) )
2		iotaex	|- ( iota x ( x e. A /\ ps ) ) e. _V
3	1 2	eqeltri	|- ( iota_ x e. A ps ) e. _V