Metamath Proof Explorer

Theorem scott0b

Description: Applying Scott's trick yields the empty set iff it was applied to the empty set. (Contributed by BTernaryTau, 3-Jul-2026)

Ref Expression
Assertion scott0b 
|- ( A = (/) <-> Scott A = (/) )

Proof

Step Hyp Ref Expression
1 scott0 
 |-  ( A = (/) <-> { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } = (/) )
2 df-scott 
 |-  Scott A = { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) }
3 2 eqeq1i 
 |-  ( Scott A = (/) <-> { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } = (/) )
4 1 3 bitr4i 
 |-  ( A = (/) <-> Scott A = (/) )