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

Theorem toponunii 18549
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 18544 . 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 1369    e. wcel 1756   U.cuni 4103   ` cfv 5430  TopOnctopon 18511
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4425  ax-nul 4433  ax-pow 4482  ax-pr 4543  ax-un 6384
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2620  df-ral 2732  df-rex 2733  df-rab 2736  df-v 2986  df-sbc 3199  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-nul 3650  df-if 3804  df-pw 3874  df-sn 3890  df-pr 3892  df-op 3896  df-uni 4104  df-br 4305  df-opab 4363  df-mpt 4364  df-id 4648  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-iota 5393  df-fun 5432  df-fv 5438  df-topon 18518
This theorem is referenced by:  indisuni  18619  indistpsx  18626  letopuni  18823  dfac14  19203  sszcld  20406  reperflem  20407  cnperf  20409  iiuni  20469  cncfcn1  20498  cncfmpt2f  20502  cdivcncf  20505  abscncfALT  20508  cncfcnvcn  20509  cnrehmeo  20537  cnheiborlem  20538  cnheibor  20539  cnllycmp  20540  bndth  20542  csscld  20773  clsocv  20774  cncmet  20845  resscdrg  20882  mbfimaopnlem  21145  limcnlp  21365  limcflflem  21367  limcflf  21368  limcmo  21369  limcres  21373  cnlimc  21375  limccnp  21378  limccnp2  21379  limciun  21381  perfdvf  21390  recnperf  21392  dvidlem  21402  dvcnp2  21406  dvcn  21407  dvnres  21417  dvaddbr  21424  dvmulbr  21425  dvcobr  21432  dvcjbr  21435  dvrec  21441  dvcnvlem  21460  dvexp3  21462  dveflem  21463  dvlipcn  21478  lhop1lem  21497  ftc1cn  21527  dvply1  21762  dvtaylp  21847  taylthlem2  21851  psercn  21903  pserdvlem2  21905  pserdv  21906  abelth  21918  logcn  22104  dvloglem  22105  logdmopn  22106  dvlog  22108  dvlog2  22110  efopnlem2  22114  logtayl  22117  cxpcn  22195  cxpcn2  22196  cxpcn3  22198  resqrcn  22199  sqrcn  22200  dvatan  22342  efrlim  22375  ftalem3  22424  blocni  24217  ipasslem8  24249  ubthlem1  24283  tpr2uni  26347  tpr2rico  26354  mndpluscn  26368  rmulccn  26370  raddcn  26371  lgamucov  27036  lgamucov2  27037  cvxscon  27144  cvmlift2lem11  27214  dvtanlem  28453  dvtan  28454  ftc1cnnc  28478  dvasin  28492  dvacos  28493  dvreasin  28494  dvreacos  28495  areacirclem2  28497  ivthALT  28542  reheibor  28750
  Copyright terms: Public domain W3C validator