Theorem toponunii 23073

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

Syntax hints:   = wceq 1570   ∈ wcel 2143  ∪ cuni 4872  ‘cfv 6536  TopOnctopon 23067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-iota 6492  df-fun 6538  df-fv 6544  df-topon 23068

This theorem is referenced by:  toponrestid  23078  indisuni  23160  indistpsx  23167  letopuni  23364  dfac14  23775  unicntop  24942  sszcld  24975  reperflem  24976  cnperf  24978  iiuni  25040  abscncfALT  25083  cncfcnvcn  25084  cnheiborlem  25113  cnheibor  25114  cnllycmp  25115  bndth  25117  mbfimaopnlem  25814  limcnlp  26037  limcflflem  26039  limcflf  26040  limcmo  26041  limcres  26045  limccnp  26050  limccnp2  26051  perfdvf  26062  recnperf  26064  dvcnp2  26079  dvaddbr  26097  dvmulbr  26098  dvcobr  26105  dvcnvlem  26135  lhop1lem  26172  taylthlem2  26537  abelth  26604  cxpcn3  26913  lgamucov  27202  ftalem3  27239  blocni  31157  ipasslem8  31189  ubthlem1  31222  tpr2uni  34295  tpr2rico  34302  mndpluscn  34316  raddcn  34319  cvxsconn  35735  cvmlift2lem11  35805  ivthALT  36846  poimir  38304  broucube  38305  ftc1cnnc  38343  dvasin  38355  dvacos  38356  dvreasin  38357  dvreacos  38358  areacirclem2  38360  reheibor  38490  islptre  46335  dirkercncf  46821  fourierdlem62  46882