Metamath Proof Explorer


Theorem iotanul

Description: Theorem 8.22 in Quine p. 57. This theorem is the result if there isn't exactly one x that satisfies ph . (Contributed by Andrew Salmon, 11-Jul-2011)

Ref Expression
Assertion iotanul ¬ ∃! x φ ι x | φ =

Proof

Step Hyp Ref Expression
1 eu6 ∃! x φ z x φ x = z
2 dfiota2 ι x | φ = z | x φ x = z
3 alnex z ¬ x φ x = z ¬ z x φ x = z
4 dfnul2 = z | ¬ z = z
5 equid z = z
6 5 tbt ¬ x φ x = z ¬ x φ x = z z = z
7 6 biimpi ¬ x φ x = z ¬ x φ x = z z = z
8 7 con1bid ¬ x φ x = z ¬ z = z x φ x = z
9 8 alimi z ¬ x φ x = z z ¬ z = z x φ x = z
10 abbi1 z ¬ z = z x φ x = z z | ¬ z = z = z | x φ x = z
11 9 10 syl z ¬ x φ x = z z | ¬ z = z = z | x φ x = z
12 4 11 syl5req z ¬ x φ x = z z | x φ x = z =
13 3 12 sylbir ¬ z x φ x = z z | x φ x = z =
14 13 unieqd ¬ z x φ x = z z | x φ x = z =
15 uni0 =
16 14 15 syl6eq ¬ z x φ x = z z | x φ x = z =
17 2 16 syl5eq ¬ z x φ x = z ι x | φ =
18 1 17 sylnbi ¬ ∃! x φ ι x | φ =