Theorem exists2 2294

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.

Step	Hyp	Ref	Expression
1		nfeu1 2214	. . . . . 6 ⊢ Ⅎx∃!x x = x
2		nfa1 1788	. . . . . 6 ⊢ Ⅎx∀xφ
3		exists1 2293	. . . . . . 7 ⊢ (∃!x x = x ↔ ∀x x = y)
4		ax16 2045	. . . . . . 7 ⊢ (∀x x = y → (φ → ∀xφ))
5	3, 4	sylbi 187	. . . . . 6 ⊢ (∃!x x = x → (φ → ∀xφ))
6	1, 2, 5	exlimd 1806	. . . . 5 ⊢ (∃!x x = x → (∃xφ → ∀xφ))
7	6	com12 27	. . . 4 ⊢ (∃xφ → (∃!x x = x → ∀xφ))
8		alex 1572	. . . 4 ⊢ (∀xφ ↔ ¬ ∃x ¬ φ)
9	7, 8	syl6ib 217	. . 3 ⊢ (∃xφ → (∃!x x = x → ¬ ∃x ¬ φ))
10	9	con2d 107	. 2 ⊢ (∃xφ → (∃x ¬ φ → ¬ ∃!x x = x))
11	10	imp 418	1 ⊢ ((∃xφ ∧ ∃x ¬ φ) → ¬ ∃!x x = x)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 358  ∀wal 1540  ∃wex 1541   = wceq 1642  ∃!weu 2204

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925

This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-eu 2208

This theorem is referenced by: (None)