Metamath Proof Explorer


Theorem emptynf

Description: On the empty domain, any variable is effectively nonfree in any formula. (Contributed by Wolf Lammen, 12-Mar-2023)

Ref Expression
Assertion emptynf ( ¬ ∃ 𝑥 ⊤ → Ⅎ 𝑥 𝜑 )

Proof

Step Hyp Ref Expression
1 emptyal ( ¬ ∃ 𝑥 ⊤ → ∀ 𝑥 𝜑 )
2 nftht ( ∀ 𝑥 𝜑 → Ⅎ 𝑥 𝜑 )
3 1 2 syl ( ¬ ∃ 𝑥 ⊤ → Ⅎ 𝑥 𝜑 )