Theorem toponunii 22899

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

Syntax hints:   = wceq 1547   ∈ wcel 2119  ∪ cuni 4838  ‘cfv 6485  TopOnctopon 22893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-iota 6441  df-fun 6487  df-fv 6493  df-topon 22894

This theorem is referenced by:  toponrestid  22904  indisuni  22986  indistpsx  22993  letopuni  23190  dfac14  23601  unicntop  24768  sszcld  24801  reperflem  24802  cnperf  24804  iiuni  24866  abscncfALT  24909  cncfcnvcn  24910  cnheiborlem  24939  cnheibor  24940  cnllycmp  24941  bndth  24943  mbfimaopnlem  25640  limcnlp  25863  limcflflem  25865  limcflf  25866  limcmo  25867  limcres  25871  limccnp  25876  limccnp2  25877  perfdvf  25888  recnperf  25890  dvcnp2  25905  dvaddbr  25923  dvmulbr  25924  dvcobr  25931  dvcnvlem  25961  lhop1lem  25998  taylthlem2  26357  abelth  26424  cxpcn3  26730  lgamucov  27019  ftalem3  27056  blocni  30894  ipasslem8  30926  ubthlem1  30959  tpr2uni  34089  tpr2rico  34096  mndpluscn  34110  raddcn  34113  cvxsconn  35471  cvmlift2lem11  35541  ivthALT  36563  poimir  38020  broucube  38021  ftc1cnnc  38059  dvasin  38071  dvacos  38072  dvreasin  38073  dvreacos  38074  areacirclem2  38076  reheibor  38206  islptre  46064  dirkercncf  46550  fourierdlem62  46611