Theorem toponunii 22425

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

Step	Hyp	Ref	Expression
1		topontopi.1	. 2 ⊢ 𝐽 ∈ (TopOn‘𝐵)
2		toponuni 22423	. 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽)
3	1, 2	ax-mp 5	1 ⊢ 𝐵 = ∪ 𝐽

Syntax hints:   = wceq 1541   ∈ wcel 2106  ∪ cuni 4908  ‘cfv 6543  TopOnctopon 22419

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-iota 6495  df-fun 6545  df-fv 6551  df-topon 22420

This theorem is referenced by:  toponrestid  22430  indisuni  22513  indistpsx  22520  letopuni  22718  dfac14  23129  unicntop  24309  sszcld  24340  reperflem  24341  cnperf  24343  iiuni  24404  abscncfALT  24447  cncfcnvcn  24448  cnheiborlem  24477  cnheibor  24478  cnllycmp  24479  bndth  24481  mbfimaopnlem  25179  limcnlp  25402  limcflflem  25404  limcflf  25405  limcmo  25406  limcres  25410  limccnp  25415  limccnp2  25416  perfdvf  25427  recnperf  25429  dvcnp2  25444  dvaddbr  25462  dvmulbr  25463  dvcobr  25470  dvcnvlem  25500  lhop1lem  25537  taylthlem2  25893  abelth  25960  cxpcn3  26263  lgamucov  26549  ftalem3  26586  blocni  30096  ipasslem8  30128  ubthlem1  30161  tpr2uni  32954  tpr2rico  32961  mndpluscn  32975  rmulccn  32977  raddcn  32978  cvxsconn  34303  cvmlift2lem11  34373  gg-dvcnp2  35243  gg-dvmulbr  35244  gg-dvcobr  35245  ivthALT  35306  poimir  36607  broucube  36608  dvtanlem  36623  ftc1cnnc  36646  dvasin  36658  dvacos  36659  dvreasin  36660  dvreacos  36661  areacirclem2  36663  reheibor  36793  islptre  44414  dirkercncf  44902  fourierdlem62  44963