MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-unif Unicode version

Definition df-unif 14253
Description: Define the uniform structure component of a uniform space. (Contributed by Mario Carneiro, 14-Aug-2015.)
Assertion
Ref Expression
df-unif

Detailed syntax breakdown of Definition df-unif
StepHypRef Expression
1 cunif 14240 . 2
2 c1 9275 . . . 4
3 c3 10364 . . . 4
42, 3cdc 10747 . . 3
54cslot 14165 . 2
61, 5wceq 1369 1
Colors of variables: wff setvar class
This definition is referenced by:  unifndx  14335  unifid  14336  ressunif  19817  tuslem  19822
  Copyright terms: Public domain W3C validator