This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem riotav

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

		Ref	Expression
	Assertion	riotav	$⊢ (ι x \in V \| φ) = (ι x \| φ)$

Step	Hyp	Ref	Expression
1		df-riota	$⊢ (ι x \in V \| φ) = (ι x \| (x \in V \land φ))$
2		vex	$⊢ x \in V$
3	2	biantrur	$⊢ φ \leftrightarrow (x \in V \land φ)$
4	3	iotabii	$⊢ (ι x \| φ) = (ι x \| (x \in V \land φ))$
5	1 4	eqtr4i	$⊢ (ι x \in V \| φ) = (ι x \| φ)$