Description: Weak version of excomim . Uses only Tarski's FOL axiom schemes. (Contributed by BTernaryTau, 23-Jun-2025)
Ref | Expression | ||
---|---|---|---|
Hypothesis | excomimw.1 | ⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ 𝜓 ) ) | |
Assertion | excomimw | ⊢ ( ∃ 𝑥 ∃ 𝑦 𝜑 → ∃ 𝑦 ∃ 𝑥 𝜑 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | excomimw.1 | ⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ 𝜓 ) ) | |
2 | 1 | notbid | ⊢ ( 𝑥 = 𝑧 → ( ¬ 𝜑 ↔ ¬ 𝜓 ) ) |
3 | 2 | alcomimw | ⊢ ( ∀ 𝑦 ∀ 𝑥 ¬ 𝜑 → ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 ) |
4 | 3 | con3i | ⊢ ( ¬ ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 → ¬ ∀ 𝑦 ∀ 𝑥 ¬ 𝜑 ) |
5 | 2exnaln | ⊢ ( ∃ 𝑥 ∃ 𝑦 𝜑 ↔ ¬ ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 ) | |
6 | 2exnaln | ⊢ ( ∃ 𝑦 ∃ 𝑥 𝜑 ↔ ¬ ∀ 𝑦 ∀ 𝑥 ¬ 𝜑 ) | |
7 | 4 5 6 | 3imtr4i | ⊢ ( ∃ 𝑥 ∃ 𝑦 𝜑 → ∃ 𝑦 ∃ 𝑥 𝜑 ) |