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

Theorem toponunii 21452
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 21450 . 2 (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = 𝐽)
31, 2ax-mp 5 1 𝐵 = 𝐽
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  wcel 2105   cuni 4830  cfv 6348  TopOnctopon 21446
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-iota 6307  df-fun 6350  df-fv 6356  df-topon 21447
This theorem is referenced by:  toponrestid  21457  indisuni  21539  indistpsx  21546  letopuni  21743  dfac14  22154  unicntop  23321  sszcld  23352  reperflem  23353  cnperf  23355  iiuni  23416  abscncfALT  23455  cncfcnvcn  23456  cnheiborlem  23485  cnheibor  23486  cnllycmp  23487  bndth  23489  mbfimaopnlem  24183  limcnlp  24403  limcflflem  24405  limcflf  24406  limcmo  24407  limcres  24411  limccnp  24416  limccnp2  24417  perfdvf  24428  recnperf  24430  dvcnp2  24444  dvaddbr  24462  dvmulbr  24463  dvcobr  24470  dvcnvlem  24500  lhop1lem  24537  taylthlem2  24889  abelth  24956  cxpcn3  25256  lgamucov  25542  ftalem3  25579  blocni  28509  ipasslem8  28541  ubthlem1  28574  tpr2uni  31047  tpr2rico  31054  mndpluscn  31068  rmulccn  31070  raddcn  31071  cvxsconn  32387  cvmlift2lem11  32457  ivthALT  33580  poimir  34806  broucube  34807  dvtanlem  34822  ftc1cnnc  34847  dvasin  34859  dvacos  34860  dvreasin  34861  dvreacos  34862  areacirclem2  34864  reheibor  34998  islptre  41776  dirkercncf  42269  fourierdlem62  42330
  Copyright terms: Public domain W3C validator