ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  exists2 Structured version   GIF version

Theorem exists2 1905
Description: A condition implying that at least two things exist. (Contributed by NM, 10-Apr-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
Assertion
Ref Expression
exists2 ((xφ x ¬ φ) → ¬ ∃!x x = x)

Proof of Theorem exists2
Dummy variable y is distinct from all other variables.
StepHypRef Expression
1 hbeu1 1822 . . . . . 6 (∃!x x = xx∃!x x = x)
2 hba1 1371 . . . . . 6 (xφxxφ)
3 exists1 1904 . . . . . . 7 (∃!x x = xx x = y)
4 ax16 1612 . . . . . . 7 (x x = y → (φxφ))
53, 4sylbi 112 . . . . . 6 (∃!x x = x → (φxφ))
61, 2, 5exlimdh 1422 . . . . 5 (∃!x x = x → (xφxφ))
76com12 25 . . . 4 (xφ → (∃!x x = xxφ))
8 alexim 1466 . . . 4 (xφ → ¬ x ¬ φ)
97, 8syl6 27 . . 3 (xφ → (∃!x x = x → ¬ x ¬ φ))
109con2d 537 . 2 (xφ → (x ¬ φ → ¬ ∃!x x = x))
1110imp 113 1 ((xφ x ¬ φ) → ¬ ∃!x x = x)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4   wa 95  wal 1271  wex 1318   = wceq 1329  ∃!weu 1812
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 97  ax-ia2 98  ax-ia3 99  ax-in1 527  ax-in2 528  ax-io 610  ax-5 1272  ax-7 1273  ax-gen 1274  ax-ie1 1319  ax-ie2 1320  ax-8 1333  ax-10 1334  ax-11 1335  ax-i12 1336  ax-4 1338  ax-17 1356  ax-i9 1360  ax-ial 1365
This theorem depends on definitions:  df-bi 108  df-tru 1195  df-fal 1196  df-nf 1286  df-sb 1565  df-eu 1815
  Copyright terms: Public domain W3C validator