Description: An equivalent expression for universal quantification over a non-occurring variable proved over ax-1 -- ax-5 . The forward implication can be strengthened when ax-6 is posited (which implies that models are non-empty), see spvw . The reverse implication can be seen as a strengthening of ax-5 (since the antecedent of the implication is weakened). See bj-exextruan for a dual statement.
An approximate meaning is: the universal quantification of a proposition over a non-occurring variable holds if and only if the proposition holds in nonempty universes. (Contributed by BJ, 14-Mar-2026) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-alextruim | ⊢ ( ∀ 𝑥 𝜑 ↔ ( ∃ 𝑥 ⊤ → 𝜑 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bj-spvw | ⊢ ( ∃ 𝑥 ⊤ → ( 𝜑 ↔ ∀ 𝑥 𝜑 ) ) | |
| 2 | 1 | biimprcd | ⊢ ( ∀ 𝑥 𝜑 → ( ∃ 𝑥 ⊤ → 𝜑 ) ) |
| 3 | ax-5 | ⊢ ( 𝜑 → ∀ 𝑥 𝜑 ) | |
| 4 | 3 | imim2i | ⊢ ( ( ∃ 𝑥 ⊤ → 𝜑 ) → ( ∃ 𝑥 ⊤ → ∀ 𝑥 𝜑 ) ) |
| 5 | 19.38 | ⊢ ( ( ∃ 𝑥 ⊤ → ∀ 𝑥 𝜑 ) → ∀ 𝑥 ( ⊤ → 𝜑 ) ) | |
| 6 | pm2.27 | ⊢ ( ⊤ → ( ( ⊤ → 𝜑 ) → 𝜑 ) ) | |
| 7 | 6 | mptru | ⊢ ( ( ⊤ → 𝜑 ) → 𝜑 ) |
| 8 | 5 7 | sylg | ⊢ ( ( ∃ 𝑥 ⊤ → ∀ 𝑥 𝜑 ) → ∀ 𝑥 𝜑 ) |
| 9 | 4 8 | syl | ⊢ ( ( ∃ 𝑥 ⊤ → 𝜑 ) → ∀ 𝑥 𝜑 ) |
| 10 | 2 9 | impbii | ⊢ ( ∀ 𝑥 𝜑 ↔ ( ∃ 𝑥 ⊤ → 𝜑 ) ) |