Metamath Proof Explorer


Theorem iotassuniOLD

Description: Obsolete version of iotassuni as of 23-Dec-2024. (Contributed by Mario Carneiro, 24-Dec-2016) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion iotassuniOLD ι 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 | φ