Description: Existential quantification over a given variable is idempotent. Weak version of bj-exexbiex , requiring fewer axioms. (Contributed by Gino Giotto, 4-Nov-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | exexw.1 | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) | |
| Assertion | exexw | ⊢ ( ∃ 𝑥 𝜑 ↔ ∃ 𝑥 ∃ 𝑥 𝜑 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | exexw.1 | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) | |
| 2 | 1 | notbid | ⊢ ( 𝑥 = 𝑦 → ( ¬ 𝜑 ↔ ¬ 𝜓 ) ) |
| 3 | 2 | hba1w | ⊢ ( ∀ 𝑥 ¬ 𝜑 → ∀ 𝑥 ∀ 𝑥 ¬ 𝜑 ) |
| 4 | 2 | spw | ⊢ ( ∀ 𝑥 ¬ 𝜑 → ¬ 𝜑 ) |
| 5 | 4 | alimi | ⊢ ( ∀ 𝑥 ∀ 𝑥 ¬ 𝜑 → ∀ 𝑥 ¬ 𝜑 ) |
| 6 | 3 5 | impbii | ⊢ ( ∀ 𝑥 ¬ 𝜑 ↔ ∀ 𝑥 ∀ 𝑥 ¬ 𝜑 ) |
| 7 | 6 | notbii | ⊢ ( ¬ ∀ 𝑥 ¬ 𝜑 ↔ ¬ ∀ 𝑥 ∀ 𝑥 ¬ 𝜑 ) |
| 8 | df-ex | ⊢ ( ∃ 𝑥 𝜑 ↔ ¬ ∀ 𝑥 ¬ 𝜑 ) | |
| 9 | 2exnaln | ⊢ ( ∃ 𝑥 ∃ 𝑥 𝜑 ↔ ¬ ∀ 𝑥 ∀ 𝑥 ¬ 𝜑 ) | |
| 10 | 7 8 9 | 3bitr4i | ⊢ ( ∃ 𝑥 𝜑 ↔ ∃ 𝑥 ∃ 𝑥 𝜑 ) |