Description: Exixtentially quantifying over a non-occurring variable is independent from the variable, under a weaker condition than in bj-cbvexvv . (Contributed by BJ, 14-Mar-2026) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-cbvaew | ⊢ ( ( ∀ 𝑥 𝜑 → ∀ 𝑦 ⊥ ) → ( ∃ 𝑦 𝜓 → ∃ 𝑥 𝜓 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | notnotb | ⊢ ( 𝜑 ↔ ¬ ¬ 𝜑 ) | |
| 2 | 1 | albii | ⊢ ( ∀ 𝑥 𝜑 ↔ ∀ 𝑥 ¬ ¬ 𝜑 ) |
| 3 | df-fal | ⊢ ( ⊥ ↔ ¬ ⊤ ) | |
| 4 | 3 | albii | ⊢ ( ∀ 𝑦 ⊥ ↔ ∀ 𝑦 ¬ ⊤ ) |
| 5 | 2 4 | imbi12i | ⊢ ( ( ∀ 𝑥 𝜑 → ∀ 𝑦 ⊥ ) ↔ ( ∀ 𝑥 ¬ ¬ 𝜑 → ∀ 𝑦 ¬ ⊤ ) ) |
| 6 | bj-exexalal | ⊢ ( ( ∃ 𝑦 ⊤ → ∃ 𝑥 ¬ 𝜑 ) ↔ ( ∀ 𝑥 ¬ ¬ 𝜑 → ∀ 𝑦 ¬ ⊤ ) ) | |
| 7 | 5 6 | bitr4i | ⊢ ( ( ∀ 𝑥 𝜑 → ∀ 𝑦 ⊥ ) ↔ ( ∃ 𝑦 ⊤ → ∃ 𝑥 ¬ 𝜑 ) ) |
| 8 | bj-cbvew | ⊢ ( ( ∃ 𝑦 ⊤ → ∃ 𝑥 ¬ 𝜑 ) → ( ∃ 𝑦 𝜓 → ∃ 𝑥 𝜓 ) ) | |
| 9 | 7 8 | sylbi | ⊢ ( ( ∀ 𝑥 𝜑 → ∀ 𝑦 ⊥ ) → ( ∃ 𝑦 𝜓 → ∃ 𝑥 𝜓 ) ) |