Description: A condition implying that at least two things exist. (Contributed by NM, 10-Apr-2004) (Proof shortened by Andrew Salmon, 9-Jul-2011) Reduce axiom usage. (Revised by Wolf Lammen, 4-Mar-2023)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | exists2 | ⊢ ( ( ∃ 𝑥 𝜑 ∧ ∃ 𝑥 ¬ 𝜑 ) → ¬ ∃! 𝑥 𝑥 = 𝑥 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | axc16nf | ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝜑 ) | |
| 2 | 1 | nfrd | ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜑 ) ) |
| 3 | 2 | com12 | ⊢ ( ∃ 𝑥 𝜑 → ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑥 𝜑 ) ) |
| 4 | exists1 | ⊢ ( ∃! 𝑥 𝑥 = 𝑥 ↔ ∀ 𝑥 𝑥 = 𝑦 ) | |
| 5 | alex | ⊢ ( ∀ 𝑥 𝜑 ↔ ¬ ∃ 𝑥 ¬ 𝜑 ) | |
| 6 | 5 | bicomi | ⊢ ( ¬ ∃ 𝑥 ¬ 𝜑 ↔ ∀ 𝑥 𝜑 ) |
| 7 | 3 4 6 | 3imtr4g | ⊢ ( ∃ 𝑥 𝜑 → ( ∃! 𝑥 𝑥 = 𝑥 → ¬ ∃ 𝑥 ¬ 𝜑 ) ) |
| 8 | 7 | con2d | ⊢ ( ∃ 𝑥 𝜑 → ( ∃ 𝑥 ¬ 𝜑 → ¬ ∃! 𝑥 𝑥 = 𝑥 ) ) |
| 9 | 8 | imp | ⊢ ( ( ∃ 𝑥 𝜑 ∧ ∃ 𝑥 ¬ 𝜑 ) → ¬ ∃! 𝑥 𝑥 = 𝑥 ) |