Metamath Proof Explorer

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 (/) C_ (/)
2 ss0 
 |-  ( Scott (/) C_ (/) -> Scott (/) = (/) )
3 1 2 ax-mp 
 |-  Scott (/) = (/)