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 ι x | φ x | φ

Proof

Step Hyp Ref Expression
1 iotauni2 y x | φ = y ι x | φ = x | φ
2 eqimss ι x | φ = x | φ ι x | φ x | φ
3 1 2 syl y x | φ = y ι x | φ x | φ
4 iotanul2 ¬ y x | φ = y ι x | φ =
5 0ss x | φ
6 4 5 eqsstrdi ¬ y x | φ = y ι x | φ x | φ
7 3 6 pm2.61i ι x | φ x | φ