Metamath Proof Explorer

Theorem bj-alextruim

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 ⊢ ∀ x φ ↔ ∃ x ⊤ → φ

Proof

Step Hyp Ref Expression
1 bj-spvw ⊢ ∃ x ⊤ → φ ↔ ∀ x φ
2 1 biimprcd ⊢ ∀ x φ → ∃ x ⊤ → φ
3 ax-5 ⊢ φ → ∀ x φ
4 3 imim2i ⊢ ∃ x ⊤ → φ → ∃ x ⊤ → ∀ x φ
5 19.38 ⊢ ∃ x ⊤ → ∀ x φ → ∀ x ⊤ → φ
6 pm2.27 ⊢ ⊤ → ⊤ → φ → φ
7 6 mptru ⊢ ⊤ → φ → φ
8 5 7 sylg ⊢ ∃ x ⊤ → ∀ x φ → ∀ x φ
9 4 8 syl ⊢ ∃ x ⊤ → φ → ∀ x φ
10 2 9 impbii ⊢ ∀ x φ ↔ ∃ x ⊤ → φ