Theorem toponunii 22074

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

Syntax hints:   = wceq 1539   ∈ wcel 2107  ∪ cuni 4840  ‘cfv 6437  TopOnctopon 22068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-iota 6395  df-fun 6439  df-fv 6445  df-topon 22069

This theorem is referenced by:  toponrestid  22079  indisuni  22162  indistpsx  22169  letopuni  22367  dfac14  22778  unicntop  23958  sszcld  23989  reperflem  23990  cnperf  23992  iiuni  24053  abscncfALT  24096  cncfcnvcn  24097  cnheiborlem  24126  cnheibor  24127  cnllycmp  24128  bndth  24130  mbfimaopnlem  24828  limcnlp  25051  limcflflem  25053  limcflf  25054  limcmo  25055  limcres  25059  limccnp  25064  limccnp2  25065  perfdvf  25076  recnperf  25078  dvcnp2  25093  dvaddbr  25111  dvmulbr  25112  dvcobr  25119  dvcnvlem  25149  lhop1lem  25186  taylthlem2  25542  abelth  25609  cxpcn3  25910  lgamucov  26196  ftalem3  26233  blocni  29176  ipasslem8  29208  ubthlem1  29241  tpr2uni  31864  tpr2rico  31871  mndpluscn  31885  rmulccn  31887  raddcn  31888  cvxsconn  33214  cvmlift2lem11  33284  ivthALT  34533  poimir  35819  broucube  35820  dvtanlem  35835  ftc1cnnc  35858  dvasin  35870  dvacos  35871  dvreasin  35872  dvreacos  35873  areacirclem2  35875  reheibor  36006  islptre  43167  dirkercncf  43655  fourierdlem62  43716