Metamath Proof Explorer

Theorem ustne0

Description: A uniform structure cannot be empty. (Contributed by Thierry Arnoux, 16-Nov-2017)

Ref Expression
Assertion ustne0 
|- ( U e. ( UnifOn ` X ) -> U =/= (/) )

Proof

Step Hyp Ref Expression
1 ustbasel 
 |-  ( U e. ( UnifOn ` X ) -> ( X X. X ) e. U )
2 1 ne0d 
 |-  ( U e. ( UnifOn ` X ) -> U =/= (/) )