Metamath Proof Explorer
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 |
⊢ ( ¬ ∃ 𝑥 ⊤ → Ⅎ 𝑥 𝜑 ) |