Theorem vuniex 7682

Description: The union of a setvar is a set. (Contributed by BJ, 3-May-2021.) (Revised by BJ, 6-Apr-2024.)

Assertion

Ref	Expression
vuniex	⊢ ∪ 𝑥 ∈ V

Proof of Theorem vuniex

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		uniex2 7681	. 2 ⊢ ∃𝑦 𝑦 = ∪ 𝑥
2	1	issetri 3457	1 ⊢ ∪ 𝑥 ∈ V

Syntax hints:   ∈ wcel 2113  Vcvv 3438  ∪ cuni 4861

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-un 7678

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-uni 4862

This theorem is referenced by:  uniexg  7683  uniuni  7705  rankuni  9773  r0weon  9920  dfac3  10029  dfac5lem4  10034  dfac5lem4OLD  10036  dfac8  10044  dfacacn  10050  kmlem2  10060  cfslb2n  10176  ttukeylem5  10421  ttukeylem6  10422  brdom7disj  10439  brdom6disj  10440  intwun  10644  wunex2  10647  fnmrc  17528  mrcfval  17529  mrisval  17551  sylow2a  19546  toprntopon  22867  distop  22937  fctop  22946  cctop  22948  ppttop  22949  epttop  22951  fncld  22964  mretopd  23034  toponmre  23035  iscnp2  23181  2ndcsep  23401  kgenf  23483  alexsubALTlem2  23990  pwsiga  34236  sigainb  34242  dmsigagen  34250  pwldsys  34263  ldsysgenld  34266  ldgenpisyslem1  34269  ddemeas  34342  brapply  36079  dfrdg4  36094  fnessref  36500  neibastop1  36502  finxpreclem2  37534  mbfresfi  37806  pwinfi  43747  pwsal  46501  intsal  46516  salexct  46520  0ome  46715