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

Metamath Proof Explorer

Definition df-unif

Description: Define the uniform structure component of a uniform space. (Contributed by Mario Carneiro, 14-Aug-2015) Use its index-independent form unifid instead. (New usage is discouraged.)

Ref Expression
Assertion df-unif 
|- UnifSet = Slot ; 1 3

Detailed syntax breakdown

Step Hyp Ref Expression
0 cunif 
 |-  UnifSet
1 c1 
 |-  1
2 c3 
 |-  3
3 1 2 cdc 
 |-  ; 1 3
4 3 cslot 
 |-  Slot ; 1 3
5 0 4 wceq 
 |-  UnifSet = Slot ; 1 3