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

Theorem toponunii 19878
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 19873 . 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 1437    e. wcel 1870   U.cuni 4222   ` cfv 5601  TopOnctopon 19849
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-sbc 3306  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-opab 4485  df-mpt 4486  df-id 4769  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-iota 5565  df-fun 5603  df-fv 5609  df-topon 19854
This theorem is referenced by:  indisuni  19949  indistpsx  19956  letopuni  20154  dfac14  20564  sszcld  21746  reperflem  21747  cnperf  21749  iiuni  21809  cncfcn1  21838  cncfmpt2f  21842  cdivcncf  21845  abscncfALT  21848  cncfcnvcn  21849  cnrehmeo  21877  cnheiborlem  21878  cnheibor  21879  cnllycmp  21880  bndth  21882  csscld  22113  clsocv  22114  cncmet  22183  resscdrg  22218  mbfimaopnlem  22488  limcnlp  22710  limcflflem  22712  limcflf  22713  limcmo  22714  limcres  22718  cnlimc  22720  limccnp  22723  limccnp2  22724  limciun  22726  perfdvf  22735  recnperf  22737  dvidlem  22747  dvcnp2  22751  dvcn  22752  dvnres  22762  dvaddbr  22769  dvmulbr  22770  dvcobr  22777  dvcjbr  22780  dvrec  22786  dvcnvlem  22805  dvexp3  22807  dveflem  22808  dvlipcn  22823  lhop1lem  22842  ftc1cn  22872  dvply1  23105  dvtaylp  23190  taylthlem2  23194  psercn  23246  pserdvlem2  23248  pserdv  23249  abelth  23261  logcn  23457  dvloglem  23458  logdmopn  23459  dvlog  23461  dvlog2  23463  efopnlem2  23467  logtayl  23470  cxpcn  23550  cxpcn2  23551  cxpcn3  23553  resqrtcn  23554  sqrtcn  23555  dvatan  23726  efrlim  23760  lgamucov  23828  lgamucov2  23829  ftalem3  23864  blocni  26291  ipasslem8  26323  ubthlem1  26357  tpr2uni  28550  tpr2rico  28557  mndpluscn  28571  rmulccn  28573  raddcn  28574  cvxscon  29754  cvmlift2lem11  29824  ivthALT  30776  poimir  31677  broucube  31678  dvtanlem  31694  dvtanlemOLD  31695  dvtan  31696  ftc1cnnc  31720  dvasin  31732  dvacos  31733  dvreasin  31734  dvreacos  31735  areacirclem2  31737  reheibor  31875  unicntop  37011  islptre  37271  cxpcncf2  37350  dirkercncf  37538  fourierdlem62  37600
  Copyright terms: Public domain W3C validator