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	$$⊢\neg \exists x\top \to Ⅎx\phi$$

Proof

Step	Hyp	Ref	Expression
1		emptyal	$$⊢\neg \exists x\top \to \forall x\phi$$
2		nftht	$$⊢\forall x\phi \to Ⅎx\phi$$
3	1 2	syl	$$⊢\neg \exists x\top \to Ⅎx\phi$$