Theorem toponunii 22801

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  ∪ cuni 4858  ‘cfv 6482  TopOnctopon 22795

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 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-iota 6438  df-fun 6484  df-fv 6490  df-topon 22796

This theorem is referenced by:  toponrestid  22806  indisuni  22888  indistpsx  22895  letopuni  23092  dfac14  23503  unicntop  24671  sszcld  24704  reperflem  24705  cnperf  24707  iiuni  24772  abscncfALT  24816  cncfcnvcn  24817  cnheiborlem  24851  cnheibor  24852  cnllycmp  24853  bndth  24855  mbfimaopnlem  25554  limcnlp  25777  limcflflem  25779  limcflf  25780  limcmo  25781  limcres  25785  limccnp  25790  limccnp2  25791  perfdvf  25802  recnperf  25804  dvcnp2  25819  dvcnp2OLD  25820  dvaddbr  25838  dvmulbr  25839  dvmulbrOLD  25840  dvcobr  25847  dvcobrOLD  25848  dvcnvlem  25878  lhop1lem  25916  taylthlem2  26280  taylthlem2OLD  26281  abelth  26349  cxpcn3  26656  lgamucov  26946  ftalem3  26983  blocni  30749  ipasslem8  30781  ubthlem1  30814  tpr2uni  33872  tpr2rico  33879  mndpluscn  33893  raddcn  33896  cvxsconn  35220  cvmlift2lem11  35290  ivthALT  36313  poimir  37637  broucube  37638  ftc1cnnc  37676  dvasin  37688  dvacos  37689  dvreasin  37690  dvreacos  37691  areacirclem2  37693  reheibor  37823  islptre  45604  dirkercncf  46092  fourierdlem62  46153