MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  toponunii Structured version   Visualization version   GIF version

Theorem toponunii 22261
Description: The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.)
Hypothesis
Ref Expression
topontopi.1 𝐽 ∈ (TopOn‘𝐵)
Assertion
Ref Expression
toponunii 𝐵 = 𝐽

Proof of Theorem toponunii
StepHypRef Expression
1 topontopi.1 . 2 𝐽 ∈ (TopOn‘𝐵)
2 toponuni 22259 . 2 (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = 𝐽)
31, 2ax-mp 5 1 𝐵 = 𝐽
Colors of variables: wff setvar class
Syntax hints:   = wceq 1541  wcel 2106   cuni 4864  cfv 6494  TopOnctopon 22255
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5255  ax-nul 5262  ax-pow 5319  ax-pr 5383  ax-un 7669
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2888  df-ral 3064  df-rex 3073  df-rab 3407  df-v 3446  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-br 5105  df-opab 5167  df-mpt 5188  df-id 5530  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-iota 6446  df-fun 6496  df-fv 6502  df-topon 22256
This theorem is referenced by:  toponrestid  22266  indisuni  22349  indistpsx  22356  letopuni  22554  dfac14  22965  unicntop  24145  sszcld  24176  reperflem  24177  cnperf  24179  iiuni  24240  abscncfALT  24283  cncfcnvcn  24284  cnheiborlem  24313  cnheibor  24314  cnllycmp  24315  bndth  24317  mbfimaopnlem  25015  limcnlp  25238  limcflflem  25240  limcflf  25241  limcmo  25242  limcres  25246  limccnp  25251  limccnp2  25252  perfdvf  25263  recnperf  25265  dvcnp2  25280  dvaddbr  25298  dvmulbr  25299  dvcobr  25306  dvcnvlem  25336  lhop1lem  25373  taylthlem2  25729  abelth  25796  cxpcn3  26097  lgamucov  26383  ftalem3  26420  blocni  29645  ipasslem8  29677  ubthlem1  29710  tpr2uni  32377  tpr2rico  32384  mndpluscn  32398  rmulccn  32400  raddcn  32401  cvxsconn  33728  cvmlift2lem11  33798  ivthALT  34796  poimir  36100  broucube  36101  dvtanlem  36116  ftc1cnnc  36139  dvasin  36151  dvacos  36152  dvreasin  36153  dvreacos  36154  areacirclem2  36156  reheibor  36287  islptre  43830  dirkercncf  44318  fourierdlem62  44379
  Copyright terms: Public domain W3C validator