Theorem toponunii 22417

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 22415	. 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽)
3	1, 2	ax-mp 5	1 ⊢ 𝐵 = ∪ 𝐽

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

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 7724

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 22412

This theorem is referenced by:  toponrestid  22422  indisuni  22505  indistpsx  22512  letopuni  22710  dfac14  23121  unicntop  24301  sszcld  24332  reperflem  24333  cnperf  24335  iiuni  24396  abscncfALT  24439  cncfcnvcn  24440  cnheiborlem  24469  cnheibor  24470  cnllycmp  24471  bndth  24473  mbfimaopnlem  25171  limcnlp  25394  limcflflem  25396  limcflf  25397  limcmo  25398  limcres  25402  limccnp  25407  limccnp2  25408  perfdvf  25419  recnperf  25421  dvcnp2  25436  dvaddbr  25454  dvmulbr  25455  dvcobr  25462  dvcnvlem  25492  lhop1lem  25529  taylthlem2  25885  abelth  25952  cxpcn3  26253  lgamucov  26539  ftalem3  26576  blocni  30053  ipasslem8  30085  ubthlem1  30118  tpr2uni  32880  tpr2rico  32887  mndpluscn  32901  rmulccn  32903  raddcn  32904  cvxsconn  34229  cvmlift2lem11  34299  gg-dvcnp2  35169  gg-dvmulbr  35170  gg-dvcobr  35171  gg-rmulccn  35174  ivthALT  35215  poimir  36516  broucube  36517  dvtanlem  36532  ftc1cnnc  36555  dvasin  36567  dvacos  36568  dvreasin  36569  dvreacos  36570  areacirclem2  36572  reheibor  36702  islptre  44325  dirkercncf  44813  fourierdlem62  44874