Theorem toponunii 20721

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

Syntax hints:   = wceq 1483   ∈ wcel 1990  ∪ cuni 4436  ‘cfv 5888  TopOnctopon 20715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-iota 5851  df-fun 5890  df-fv 5896  df-topon 20716

This theorem is referenced by:  indisuni  20807  indistpsx  20814  letopuni  21011  dfac14  21421  unicntop  22589  sszcld  22620  reperflem  22621  cnperf  22623  iiuni  22684  cncfcn1  22713  cncfmpt2f  22717  cdivcncf  22720  abscncfALT  22723  cncfcnvcn  22724  cnrehmeo  22752  cnheiborlem  22753  cnheibor  22754  cnllycmp  22755  bndth  22757  csscld  23048  clsocv  23049  cncmet  23119  resscdrg  23154  mbfimaopnlem  23422  limcnlp  23642  limcflflem  23644  limcflf  23645  limcmo  23646  limcres  23650  cnlimc  23652  limccnp  23655  limccnp2  23656  limciun  23658  perfdvf  23667  recnperf  23669  dvidlem  23679  dvcnp2  23683  dvcn  23684  dvnres  23694  dvaddbr  23701  dvmulbr  23702  dvcobr  23709  dvcjbr  23712  dvrec  23718  dvcnvlem  23739  dvexp3  23741  dveflem  23742  dvlipcn  23757  lhop1lem  23776  ftc1cn  23806  dvply1  24039  dvtaylp  24124  taylthlem2  24128  psercn  24180  pserdvlem2  24182  pserdv  24183  abelth  24195  logcn  24393  dvloglem  24394  logdmopn  24395  dvlog  24397  dvlog2  24399  efopnlem2  24403  logtayl  24406  cxpcn  24486  cxpcn2  24487  cxpcn3  24489  resqrtcn  24490  sqrtcn  24491  dvatan  24662  efrlim  24696  lgamucov  24764  lgamucov2  24765  ftalem3  24801  blocni  27660  ipasslem8  27692  ubthlem1  27726  tpr2uni  29951  tpr2rico  29958  mndpluscn  29972  rmulccn  29974  raddcn  29975  cxpcncf1  30673  cvxsconn  31225  cvmlift2lem11  31295  ivthALT  32330  knoppcnlem10  32492  knoppcnlem11  32493  poimir  33442  broucube  33443  dvtanlem  33459  dvtan  33460  ftc1cnnc  33484  dvasin  33496  dvacos  33497  dvreasin  33498  dvreacos  33499  areacirclem2  33501  reheibor  33638  islptre  39851  cxpcncf2  40113  dirkercncf  40324  fourierdlem62  40385