Theorem toponunii 21785

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

Syntax hints:   = wceq 1543   ∈ wcel 2110  ∪ cuni 4809  ‘cfv 6369  TopOnctopon 21779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2706  ax-sep 5181  ax-nul 5188  ax-pow 5247  ax-pr 5311  ax-un 7512

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2537  df-eu 2566  df-clab 2713  df-cleq 2726  df-clel 2812  df-nfc 2882  df-ne 2936  df-ral 3059  df-rex 3060  df-rab 3063  df-v 3403  df-sbc 3688  df-dif 3860  df-un 3862  df-in 3864  df-ss 3874  df-nul 4228  df-if 4430  df-pw 4505  df-sn 4532  df-pr 4534  df-op 4538  df-uni 4810  df-br 5044  df-opab 5106  df-mpt 5125  df-id 5444  df-xp 5546  df-rel 5547  df-cnv 5548  df-co 5549  df-dm 5550  df-iota 6327  df-fun 6371  df-fv 6377  df-topon 21780

This theorem is referenced by:  toponrestid  21790  indisuni  21872  indistpsx  21879  letopuni  22076  dfac14  22487  unicntop  23655  sszcld  23686  reperflem  23687  cnperf  23689  iiuni  23750  abscncfALT  23793  cncfcnvcn  23794  cnheiborlem  23823  cnheibor  23824  cnllycmp  23825  bndth  23827  mbfimaopnlem  24524  limcnlp  24747  limcflflem  24749  limcflf  24750  limcmo  24751  limcres  24755  limccnp  24760  limccnp2  24761  perfdvf  24772  recnperf  24774  dvcnp2  24789  dvaddbr  24807  dvmulbr  24808  dvcobr  24815  dvcnvlem  24845  lhop1lem  24882  taylthlem2  25238  abelth  25305  cxpcn3  25606  lgamucov  25892  ftalem3  25929  blocni  28858  ipasslem8  28890  ubthlem1  28923  tpr2uni  31541  tpr2rico  31548  mndpluscn  31562  rmulccn  31564  raddcn  31565  cvxsconn  32890  cvmlift2lem11  32960  ivthALT  34218  poimir  35504  broucube  35505  dvtanlem  35520  ftc1cnnc  35543  dvasin  35555  dvacos  35556  dvreasin  35557  dvreacos  35558  areacirclem2  35560  reheibor  35691  islptre  42789  dirkercncf  43277  fourierdlem62  43338