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

Theorem toponunii 19940
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 19935 . 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 1443    e. wcel 1886   U.cuni 4197   ` cfv 5581  TopOnctopon 19911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3046  df-sbc 3267  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-op 3974  df-uni 4198  df-br 4402  df-opab 4461  df-mpt 4462  df-id 4748  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-iota 5545  df-fun 5583  df-fv 5589  df-topon 19916
This theorem is referenced by:  indisuni  20011  indistpsx  20018  letopuni  20216  dfac14  20626  sszcld  21828  reperflem  21829  cnperf  21831  iiuni  21906  cncfcn1  21935  cncfmpt2f  21939  cdivcncf  21942  abscncfALT  21945  cncfcnvcn  21946  cnrehmeo  21974  cnheiborlem  21975  cnheibor  21976  cnllycmp  21977  bndth  21979  csscld  22213  clsocv  22214  cncmet  22283  resscdrg  22318  mbfimaopnlem  22604  limcnlp  22826  limcflflem  22828  limcflf  22829  limcmo  22830  limcres  22834  cnlimc  22836  limccnp  22839  limccnp2  22840  limciun  22842  perfdvf  22851  recnperf  22853  dvidlem  22863  dvcnp2  22867  dvcn  22868  dvnres  22878  dvaddbr  22885  dvmulbr  22886  dvcobr  22893  dvcjbr  22896  dvrec  22902  dvcnvlem  22921  dvexp3  22923  dveflem  22924  dvlipcn  22939  lhop1lem  22958  ftc1cn  22988  dvply1  23230  dvtaylp  23318  taylthlem2  23322  psercn  23374  pserdvlem2  23376  pserdv  23377  abelth  23389  logcn  23585  dvloglem  23586  logdmopn  23587  dvlog  23589  dvlog2  23591  efopnlem2  23595  logtayl  23598  cxpcn  23678  cxpcn2  23679  cxpcn3  23681  resqrtcn  23682  sqrtcn  23683  dvatan  23854  efrlim  23888  lgamucov  23956  lgamucov2  23957  ftalem3  23992  blocni  26439  ipasslem8  26471  ubthlem1  26505  tpr2uni  28704  tpr2rico  28711  mndpluscn  28725  rmulccn  28727  raddcn  28728  cvxscon  29959  cvmlift2lem11  30029  ivthALT  30984  poimir  31966  broucube  31967  dvtanlem  31983  dvtanlemOLD  31984  dvtan  31985  ftc1cnnc  32009  dvasin  32021  dvacos  32022  dvreasin  32023  dvreacos  32024  areacirclem2  32026  reheibor  32164  unicntop  37365  islptre  37693  cxpcncf2  37772  dirkercncf  37963  fourierdlem62  38026
  Copyright terms: Public domain W3C validator