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

Theorem toponunii 18437
Description: The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.)
Hypothesis
Ref Expression
topontopi.1  |-  J  e.  (TopOn `  B )
Assertion
Ref Expression
toponunii  |-  B  = 
U. J

Proof of Theorem toponunii
StepHypRef Expression
1 topontopi.1 . 2  |-  J  e.  (TopOn `  B )
2 toponuni 18432 . 2  |-  ( J  e.  (TopOn `  B
)  ->  B  =  U. J )
31, 2ax-mp 5 1  |-  B  = 
U. J
Colors of variables: wff setvar class
Syntax hints:    = wceq 1364    e. wcel 1761   U.cuni 4088   ` cfv 5415  TopOnctopon 18399
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2263  df-mo 2264  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-sbc 3184  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-br 4290  df-opab 4348  df-mpt 4349  df-id 4632  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-iota 5378  df-fun 5417  df-fv 5423  df-topon 18406
This theorem is referenced by:  indisuni  18507  indistpsx  18514  letopuni  18711  dfac14  19091  sszcld  20294  reperflem  20295  cnperf  20297  iiuni  20357  cncfcn1  20386  cncfmpt2f  20390  cdivcncf  20393  abscncfALT  20396  cncfcnvcn  20397  cnrehmeo  20425  cnheiborlem  20426  cnheibor  20427  cnllycmp  20428  bndth  20430  csscld  20661  clsocv  20662  cncmet  20733  resscdrg  20770  mbfimaopnlem  21033  limcnlp  21253  limcflflem  21255  limcflf  21256  limcmo  21257  limcres  21261  cnlimc  21263  limccnp  21266  limccnp2  21267  limciun  21269  perfdvf  21278  recnperf  21280  dvidlem  21290  dvcnp2  21294  dvcn  21295  dvnres  21305  dvaddbr  21312  dvmulbr  21313  dvcobr  21320  dvcjbr  21323  dvrec  21329  dvcnvlem  21348  dvexp3  21350  dveflem  21351  dvlipcn  21366  lhop1lem  21385  ftc1cn  21415  dvply1  21693  dvtaylp  21778  taylthlem2  21782  psercn  21834  pserdvlem2  21836  pserdv  21837  abelth  21849  logcn  22035  dvloglem  22036  logdmopn  22037  dvlog  22039  dvlog2  22041  efopnlem2  22045  logtayl  22048  cxpcn  22126  cxpcn2  22127  cxpcn3  22129  resqrcn  22130  sqrcn  22131  dvatan  22273  efrlim  22306  ftalem3  22355  blocni  24124  ipasslem8  24156  ubthlem1  24190  tpr2uni  26255  tpr2rico  26262  mndpluscn  26276  rmulccn  26278  raddcn  26279  lgamucov  26938  lgamucov2  26939  cvxscon  27046  cvmlift2lem11  27116  dvtanlem  28350  dvtan  28351  ftc1cnnc  28375  dvasin  28389  dvacos  28390  dvreasin  28391  dvreacos  28392  areacirclem2  28394  ivthALT  28439  reheibor  28647
  Copyright terms: Public domain W3C validator