Theorem scott0

Description: Applying Scott's trick to the empty set leaves it unchanged. (Contributed by BTernaryTau, 3-Jul-2026)

	Ref	Expression
Assertion	scott0	$$⊢Scott\varnothing =\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		scottss	$$⊢Scott\varnothing \subseteq \varnothing$$
2		ss0	$$⊢Scott\varnothing \subseteq \varnothing \to Scott\varnothing =\varnothing$$
3	1 2	ax-mp	$$⊢Scott\varnothing =\varnothing$$