Metamath Proof Explorer

Theorem riotav

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

Ref Expression
Assertion riotav 
|- ( iota_ x e. _V ph ) = ( iota x ph )

Proof

Step Hyp Ref Expression
1 df-riota 
 |-  ( iota_ x e. _V ph ) = ( iota x ( x e. _V /\ ph ) )
2 vex 
 |-  x e. _V
3 2 biantrur 
 |-  ( ph <-> ( x e. _V /\ ph ) )
4 3 iotabii 
 |-  ( iota x ph ) = ( iota x ( x e. _V /\ ph ) )
5 1 4 eqtr4i 
 |-  ( iota_ x e. _V ph ) = ( iota x ph )