Theorem toponunii 22859

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  ∪ cuni 4888  ‘cfv 6536  TopOnctopon 22853

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 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734

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 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-iota 6489  df-fun 6538  df-fv 6544  df-topon 22854

This theorem is referenced by:  toponrestid  22864  indisuni  22946  indistpsx  22953  letopuni  23150  dfac14  23561  unicntop  24729  sszcld  24762  reperflem  24763  cnperf  24765  iiuni  24830  abscncfALT  24874  cncfcnvcn  24875  cnheiborlem  24909  cnheibor  24910  cnllycmp  24911  bndth  24913  mbfimaopnlem  25613  limcnlp  25836  limcflflem  25838  limcflf  25839  limcmo  25840  limcres  25844  limccnp  25849  limccnp2  25850  perfdvf  25861  recnperf  25863  dvcnp2  25878  dvcnp2OLD  25879  dvaddbr  25897  dvmulbr  25898  dvmulbrOLD  25899  dvcobr  25906  dvcobrOLD  25907  dvcnvlem  25937  lhop1lem  25975  taylthlem2  26339  taylthlem2OLD  26340  abelth  26408  cxpcn3  26715  lgamucov  27005  ftalem3  27042  blocni  30791  ipasslem8  30823  ubthlem1  30856  tpr2uni  33941  tpr2rico  33948  mndpluscn  33962  raddcn  33965  cvxsconn  35270  cvmlift2lem11  35340  ivthALT  36358  poimir  37682  broucube  37683  ftc1cnnc  37721  dvasin  37733  dvacos  37734  dvreasin  37735  dvreacos  37736  areacirclem2  37738  reheibor  37868  islptre  45628  dirkercncf  46116  fourierdlem62  46177