Theorem toponunii 22894

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  ∪ cuni 4851  ‘cfv 6493  TopOnctopon 22888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-iota 6449  df-fun 6495  df-fv 6501  df-topon 22889

This theorem is referenced by:  toponrestid  22899  indisuni  22981  indistpsx  22988  letopuni  23185  dfac14  23596  unicntop  24763  sszcld  24796  reperflem  24797  cnperf  24799  iiuni  24861  abscncfALT  24904  cncfcnvcn  24905  cnheiborlem  24934  cnheibor  24935  cnllycmp  24936  bndth  24938  mbfimaopnlem  25635  limcnlp  25858  limcflflem  25860  limcflf  25861  limcmo  25862  limcres  25866  limccnp  25871  limccnp2  25872  perfdvf  25883  recnperf  25885  dvcnp2  25900  dvaddbr  25918  dvmulbr  25919  dvcobr  25926  dvcnvlem  25956  lhop1lem  25993  taylthlem2  26354  taylthlem2OLD  26355  abelth  26422  cxpcn3  26728  lgamucov  27018  ftalem3  27055  blocni  30894  ipasslem8  30926  ubthlem1  30959  tpr2uni  34068  tpr2rico  34075  mndpluscn  34089  raddcn  34092  cvxsconn  35444  cvmlift2lem11  35514  ivthALT  36536  poimir  37991  broucube  37992  ftc1cnnc  38030  dvasin  38042  dvacos  38043  dvreasin  38044  dvreacos  38045  areacirclem2  38047  reheibor  38177  islptre  46070  dirkercncf  46556  fourierdlem62  46617