Theorem toponunii 22836

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  ∪ cuni 4867  ‘cfv 6499  TopOnctopon 22830

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-iota 6452  df-fun 6501  df-fv 6507  df-topon 22831

This theorem is referenced by:  toponrestid  22841  indisuni  22923  indistpsx  22930  letopuni  23127  dfac14  23538  unicntop  24706  sszcld  24739  reperflem  24740  cnperf  24742  iiuni  24807  abscncfALT  24851  cncfcnvcn  24852  cnheiborlem  24886  cnheibor  24887  cnllycmp  24888  bndth  24890  mbfimaopnlem  25589  limcnlp  25812  limcflflem  25814  limcflf  25815  limcmo  25816  limcres  25820  limccnp  25825  limccnp2  25826  perfdvf  25837  recnperf  25839  dvcnp2  25854  dvcnp2OLD  25855  dvaddbr  25873  dvmulbr  25874  dvmulbrOLD  25875  dvcobr  25882  dvcobrOLD  25883  dvcnvlem  25913  lhop1lem  25951  taylthlem2  26315  taylthlem2OLD  26316  abelth  26384  cxpcn3  26691  lgamucov  26981  ftalem3  27018  blocni  30784  ipasslem8  30816  ubthlem1  30849  tpr2uni  33888  tpr2rico  33895  mndpluscn  33909  raddcn  33912  cvxsconn  35223  cvmlift2lem11  35293  ivthALT  36316  poimir  37640  broucube  37641  ftc1cnnc  37679  dvasin  37691  dvacos  37692  dvreasin  37693  dvreacos  37694  areacirclem2  37696  reheibor  37826  islptre  45610  dirkercncf  46098  fourierdlem62  46159