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)

Ref Expression
Assertion iotassuni ιx|φx|φ

Proof

Step Hyp Ref Expression
1 iotauni ∃!xφιx|φ=x|φ
2 eqimss ιx|φ=x|φιx|φx|φ
3 1 2 syl ∃!xφιx|φx|φ
4 iotanul ¬∃!xφιx|φ=
5 0ss x|φ
6 4 5 eqsstrdi ¬∃!xφιx|φx|φ
7 3 6 pm2.61i ιx|φx|φ