Theorem toponunii 22923

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

Syntax hints:   = wceq 1539   ∈ wcel 2107  ∪ cuni 4906  ‘cfv 6560  TopOnctopon 22917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-opab 5205  df-mpt 5225  df-id 5577  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-iota 6513  df-fun 6562  df-fv 6568  df-topon 22918

This theorem is referenced by:  toponrestid  22928  indisuni  23011  indistpsx  23018  letopuni  23216  dfac14  23627  unicntop  24807  sszcld  24840  reperflem  24841  cnperf  24843  iiuni  24908  abscncfALT  24952  cncfcnvcn  24953  cnheiborlem  24987  cnheibor  24988  cnllycmp  24989  bndth  24991  mbfimaopnlem  25691  limcnlp  25914  limcflflem  25916  limcflf  25917  limcmo  25918  limcres  25922  limccnp  25927  limccnp2  25928  perfdvf  25939  recnperf  25941  dvcnp2  25956  dvcnp2OLD  25957  dvaddbr  25975  dvmulbr  25976  dvmulbrOLD  25977  dvcobr  25984  dvcobrOLD  25985  dvcnvlem  26015  lhop1lem  26053  taylthlem2  26417  taylthlem2OLD  26418  abelth  26486  cxpcn3  26792  lgamucov  27082  ftalem3  27119  blocni  30825  ipasslem8  30857  ubthlem1  30890  tpr2uni  33905  tpr2rico  33912  mndpluscn  33926  raddcn  33929  cvxsconn  35249  cvmlift2lem11  35319  ivthALT  36337  poimir  37661  broucube  37662  ftc1cnnc  37700  dvasin  37712  dvacos  37713  dvreasin  37714  dvreacos  37715  areacirclem2  37717  reheibor  37847  islptre  45639  dirkercncf  46127  fourierdlem62  46188