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

Metamath Proof Explorer

Theorem iotanul2

Description: Version of iotanul using df-iota instead of dfiota2 . (Contributed by SN, 6-Nov-2024)

Ref Expression
Assertion iotanul2 
|- ( -. E. y { x | ph } = { y } -> ( iota x ph ) = (/) )

Proof

Step Hyp Ref Expression
1 df-iota 
 |-  ( iota x ph ) = U. { w | { x | ph } = { w } }
2 n0 
 |-  ( U. { w | { x | ph } = { w } } =/= (/) <-> E. v v e. U. { w | { x | ph } = { w } } )
3 eluni 
 |-  ( v e. U. { w | { x | ph } = { w } } <-> E. y ( v e. y /\ y e. { w | { x | ph } = { w } } ) )
4 vex 
 |-  y e. _V
5 sneq 
 |-  ( w = y -> { w } = { y } )
6 5 eqeq2d 
 |-  ( w = y -> ( { x | ph } = { w } <-> { x | ph } = { y } ) )
7 4 6 elab 
 |-  ( y e. { w | { x | ph } = { w } } <-> { x | ph } = { y } )
8 7 biimpi 
 |-  ( y e. { w | { x | ph } = { w } } -> { x | ph } = { y } )
9 8 adantl 
 |-  ( ( v e. y /\ y e. { w | { x | ph } = { w } } ) -> { x | ph } = { y } )
10 9 eximi 
 |-  ( E. y ( v e. y /\ y e. { w | { x | ph } = { w } } ) -> E. y { x | ph } = { y } )
11 3 10 sylbi 
 |-  ( v e. U. { w | { x | ph } = { w } } -> E. y { x | ph } = { y } )
12 11 exlimiv 
 |-  ( E. v v e. U. { w | { x | ph } = { w } } -> E. y { x | ph } = { y } )
13 2 12 sylbi 
 |-  ( U. { w | { x | ph } = { w } } =/= (/) -> E. y { x | ph } = { y } )
14 13 necon1bi 
 |-  ( -. E. y { x | ph } = { y } -> U. { w | { x | ph } = { w } } = (/) )
15 1 14 eqtrid 
 |-  ( -. E. y { x | ph } = { y } -> ( iota x ph ) = (/) )