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 TopOn B
Assertion toponunii B = J


Step Hyp Ref Expression
1 topontopi.1 J TopOn B
2 toponuni J TopOn B B = J
3 1 2 ax-mp B = J