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 abbi ⊢∀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 eqtr2id ⊢∀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 eqtrdi ⊢¬∃z∀xφ↔x=z→⋃z|∀xφ↔x=z=∅
17 2 16 eqtrid ⊢¬∃z∀xφ↔x=z→ιx|φ=∅
18 1 17 sylnbi ⊢¬∃!xφ→ιx|φ=∅