Theorem toponunii 22938

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

Syntax hints:   = wceq 1537   ∈ wcel 2106  ∪ cuni 4912  ‘cfv 6563  TopOnctopon 22932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-iota 6516  df-fun 6565  df-fv 6571  df-topon 22933

This theorem is referenced by:  toponrestid  22943  indisuni  23026  indistpsx  23033  letopuni  23231  dfac14  23642  unicntop  24822  sszcld  24853  reperflem  24854  cnperf  24856  iiuni  24921  abscncfALT  24965  cncfcnvcn  24966  cnheiborlem  25000  cnheibor  25001  cnllycmp  25002  bndth  25004  mbfimaopnlem  25704  limcnlp  25928  limcflflem  25930  limcflf  25931  limcmo  25932  limcres  25936  limccnp  25941  limccnp2  25942  perfdvf  25953  recnperf  25955  dvcnp2  25970  dvcnp2OLD  25971  dvaddbr  25989  dvmulbr  25990  dvmulbrOLD  25991  dvcobr  25998  dvcobrOLD  25999  dvcnvlem  26029  lhop1lem  26067  taylthlem2  26431  taylthlem2OLD  26432  abelth  26500  cxpcn3  26806  lgamucov  27096  ftalem3  27133  blocni  30834  ipasslem8  30866  ubthlem1  30899  tpr2uni  33866  tpr2rico  33873  mndpluscn  33887  raddcn  33890  cvxsconn  35228  cvmlift2lem11  35298  ivthALT  36318  poimir  37640  broucube  37641  dvtanlem  37656  ftc1cnnc  37679  dvasin  37691  dvacos  37692  dvreasin  37693  dvreacos  37694  areacirclem2  37696  reheibor  37826  islptre  45575  dirkercncf  46063  fourierdlem62  46124