Metamath Proof Explorer

Theorem elscottn0

Description: If the input class has elements, then the Scott's trick set is not empty. (Contributed by BTernaryTau, 23-Aug-2026)

Ref Expression
Assertion elscottn0 
|- ( A e. B -> Scott B =/= (/) )

Proof

Step Hyp Ref Expression
1 ne0i 
 |-  ( A e. B -> B =/= (/) )
2 scott0b 
 |-  ( B = (/) <-> Scott B = (/) )
3 2 necon3bii 
 |-  ( B =/= (/) <-> Scott B =/= (/) )
4 1 3 sylib 
 |-  ( A e. B -> Scott B =/= (/) )