Theorem scott0i

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

	Ref	Expression
Assertion	scott0i	⊢ Scott ∅ = ∅

Proof

Step	Hyp	Ref	Expression
1		scottss	⊢ Scott ∅ ⊆ ∅
2		ss0	⊢ ( Scott ∅ ⊆ ∅ → Scott ∅ = ∅ )
3	1 2	ax-mp	⊢ Scott ∅ = ∅