Metamath Proof Explorer

Theorem iotan0aiotaex

Description: If the iota over a wff ph is not empty, the alternate iota over ph is a set. (Contributed by AV, 25-Aug-2022)

Ref Expression
Assertion iotan0aiotaex 
|- ( ( iota x ph ) =/= (/) -> ( iota' x ph ) e. _V )

Proof

Step Hyp Ref Expression
1 iotanul 
 |-  ( -. E! x ph -> ( iota x ph ) = (/) )
2 1 necon1ai 
 |-  ( ( iota x ph ) =/= (/) -> E! x ph )
3 aiotaexb 
 |-  ( E! x ph <-> ( iota' x ph ) e. _V )
4 2 3 sylib 
 |-  ( ( iota x ph ) =/= (/) -> ( iota' x ph ) e. _V )