Metamath Proof Explorer

Theorem toponunii

Description: The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015)

Ref Expression
Hypothesis topontopi.1 
|- J e. ( TopOn ` B )
Assertion toponunii 
|- B = U. J

Proof

Step Hyp Ref Expression
1 topontopi.1 
 |-  J e. ( TopOn ` B )
2 toponuni 
 |-  ( J e. ( TopOn ` B ) -> B = U. J )
3 1 2 ax-mp 
 |-  B = U. J