Theorem wl-nax6al 33842

Description: In an empty domain the for-all operator always holds, even when applied to a false expression. This theorem actually shows that ax-5 2009 is provable there. Also we cannot assume that sp 2224 generally holds, except of course in the form of sptruw 1905. Without the support of an sp 2224 like theorem it seems difficult, if not impossible, to arrive at a theorem allowing to change the bounded variable in the antecedent. Additional axioms need to be postulated to further strengthen this result.

A consequence of this result is that ∃𝑥𝜑 is not true for any 𝜑. In particular, ∃*𝑥𝜑 does not hold either, a somewhat counterintuitive result. (Contributed by Wolf Lammen, 12-Mar-2023.)

Assertion

Ref	Expression
wl-nax6al	⊢ (¬ ∃𝑥⊤ → ∀𝑥𝜑)

Proof of Theorem wl-nax6al

Step	Hyp	Ref	Expression
1		trud 1667	. . . 4 ⊢ (¬ 𝜑 → ⊤)
2	1	eximi 1933	. . 3 ⊢ (∃𝑥 ¬ 𝜑 → ∃𝑥⊤)
3	2	con3i 152	. 2 ⊢ (¬ ∃𝑥⊤ → ¬ ∃𝑥 ¬ 𝜑)
4		alex 1924	. 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
5	3, 4	sylibr 226	1 ⊢ (¬ ∃𝑥⊤ → ∀𝑥𝜑)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1654  ⊤wtru 1657  ∃wex 1878

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908

This theorem depends on definitions:  df-bi 199  df-tru 1660  df-ex 1879

This theorem is referenced by:  wl-nax6nfr  33843