Description: The iota class is a subset of the union of all elements satisfying ph . (Contributed by Mario Carneiro, 24-Dec-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | iotassuni | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iotauni | |
|
2 | eqimss | |
|
3 | 1 2 | syl | |
4 | iotanul | |
|
5 | 0ss | |
|
6 | 4 5 | eqsstrdi | |
7 | 3 6 | pm2.61i | |