Theorem riotav

Description: An iota restricted to the universe is unrestricted. (Contributed by NM, 18-Sep-2011)

	Ref	Expression
Assertion	riotav	$$⊢\left(\iota x\in \mathrm{V}|\phi \right)=\left(\iota x|\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		df-riota	$$⊢\left(\iota x\in \mathrm{V}|\phi \right)=\left(\iota x|\left(x\in \mathrm{V}\wedge \phi \right)\right)$$
2		vex	$$⊢x\in \mathrm{V}$$
3	2	biantrur	$$⊢\phi \leftrightarrow \left(x\in \mathrm{V}\wedge \phi \right)$$
4	3	iotabii	$$⊢\left(\iota x|\phi \right)=\left(\iota x|\left(x\in \mathrm{V}\wedge \phi \right)\right)$$
5	1 4	eqtr4i	$$⊢\left(\iota x\in \mathrm{V}|\phi \right)=\left(\iota x|\phi \right)$$