This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ustne0

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

		Ref	Expression
	Assertion	ustne0	$⊢ U \in UnifOn (X) \to U \neq \emptyset$

Step	Hyp	Ref	Expression
1		ustbasel	$⊢ U \in UnifOn (X) \to X \times X \in U$
2	1	ne0d	$⊢ U \in UnifOn (X) \to U \neq \emptyset$