Metamath Proof Explorer


Theorem iotassuni

Description: The iota class is a subset of the union of all elements satisfying ph . (Contributed by Mario Carneiro, 24-Dec-2016) Remove dependency on ax-10 , ax-11 , ax-12 . (Revised by SN, 6-Nov-2024)

Ref Expression
Assertion iotassuni
|- ( iota x ph ) C_ U. { x | ph }

Proof

Step Hyp Ref Expression
1 iotauni2
 |-  ( E. y { x | ph } = { y } -> ( iota x ph ) = U. { x | ph } )
2 eqimss
 |-  ( ( iota x ph ) = U. { x | ph } -> ( iota x ph ) C_ U. { x | ph } )
3 1 2 syl
 |-  ( E. y { x | ph } = { y } -> ( iota x ph ) C_ U. { x | ph } )
4 iotanul2
 |-  ( -. E. y { x | ph } = { y } -> ( iota x ph ) = (/) )
5 0ss
 |-  (/) C_ U. { x | ph }
6 4 5 eqsstrdi
 |-  ( -. E. y { x | ph } = { y } -> ( iota x ph ) C_ U. { x | ph } )
7 3 6 pm2.61i
 |-  ( iota x ph ) C_ U. { x | ph }