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

Theorem toponunii 20921
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 20919 . 2 (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = 𝐽)
31, 2ax-mp 5 1 𝐵 = 𝐽
Colors of variables: wff setvar class
Syntax hints:   = wceq 1630  wcel 2137   cuni 4586  cfv 6047  TopOnctopon 20915
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-8 2139  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-sep 4931  ax-nul 4939  ax-pow 4990  ax-pr 5053  ax-un 7112
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-mo 2610  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ne 2931  df-ral 3053  df-rex 3054  df-rab 3057  df-v 3340  df-sbc 3575  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-nul 4057  df-if 4229  df-pw 4302  df-sn 4320  df-pr 4322  df-op 4326  df-uni 4587  df-br 4803  df-opab 4863  df-mpt 4880  df-id 5172  df-xp 5270  df-rel 5271  df-cnv 5272  df-co 5273  df-dm 5274  df-iota 6010  df-fun 6049  df-fv 6055  df-topon 20916
This theorem is referenced by:  indisuni  21007  indistpsx  21014  letopuni  21211  dfac14  21621  unicntop  22788  sszcld  22819  reperflem  22820  cnperf  22822  iiuni  22883  cncfcn1  22912  cncfmpt2f  22916  cdivcncf  22919  abscncfALT  22922  cncfcnvcn  22923  cnrehmeo  22951  cnheiborlem  22952  cnheibor  22953  cnllycmp  22954  bndth  22956  csscld  23246  clsocv  23247  cncmet  23317  resscdrg  23352  mbfimaopnlem  23619  limcnlp  23839  limcflflem  23841  limcflf  23842  limcmo  23843  limcres  23847  cnlimc  23849  limccnp  23852  limccnp2  23853  limciun  23855  perfdvf  23864  recnperf  23866  dvidlem  23876  dvcnp2  23880  dvcn  23881  dvnres  23891  dvaddbr  23898  dvmulbr  23899  dvcobr  23906  dvcjbr  23909  dvrec  23915  dvcnvlem  23936  dvexp3  23938  dveflem  23939  dvlipcn  23954  lhop1lem  23973  ftc1cn  24003  dvply1  24236  dvtaylp  24321  taylthlem2  24325  psercn  24377  pserdvlem2  24379  pserdv  24380  abelth  24392  logcn  24590  dvloglem  24591  logdmopn  24592  dvlog  24594  dvlog2  24596  efopnlem2  24600  logtayl  24603  cxpcn  24683  cxpcn2  24684  cxpcn3  24686  resqrtcn  24687  sqrtcn  24688  dvatan  24859  efrlim  24893  lgamucov  24961  lgamucov2  24962  ftalem3  24998  blocni  27967  ipasslem8  27999  ubthlem1  28033  tpr2uni  30258  tpr2rico  30265  mndpluscn  30279  rmulccn  30281  raddcn  30282  cxpcncf1  30980  cvxsconn  31530  cvmlift2lem11  31600  ivthALT  32634  knoppcnlem10  32796  knoppcnlem11  32797  poimir  33753  broucube  33754  dvtanlem  33770  dvtan  33771  ftc1cnnc  33795  dvasin  33807  dvacos  33808  dvreasin  33809  dvreacos  33810  areacirclem2  33812  reheibor  33949  islptre  40352  cxpcncf2  40614  dirkercncf  40825  fourierdlem62  40886
  Copyright terms: Public domain W3C validator