Theorem vuniex 7728

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 7727	. 2 ⊢ ∃𝑦 𝑦 = ∪ 𝑥
2	1	issetri 3490	1 ⊢ ∪ 𝑥 ∈ V

Syntax hints:   ∈ wcel 2106  Vcvv 3474  ∪ cuni 4908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5299  ax-un 7724

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-uni 4909

This theorem is referenced by:  uniexg  7729  uniuni  7748  rankuni  9857  r0weon  10006  dfac3  10115  dfac5lem4  10120  dfac8  10129  dfacacn  10135  kmlem2  10145  cfslb2n  10262  ttukeylem5  10507  ttukeylem6  10508  brdom7disj  10525  brdom6disj  10526  intwun  10729  wunex2  10732  fnmrc  17550  mrcfval  17551  mrisval  17573  sylow2a  19486  toprntopon  22426  distop  22497  fctop  22506  cctop  22508  ppttop  22509  epttop  22511  fncld  22525  mretopd  22595  toponmre  22596  iscnp2  22742  2ndcsep  22962  kgenf  23044  alexsubALTlem2  23551  pwsiga  33123  sigainb  33129  dmsigagen  33137  pwldsys  33150  ldsysgenld  33153  ldgenpisyslem1  33156  ddemeas  33229  brapply  34905  dfrdg4  34918  fnessref  35237  neibastop1  35239  finxpreclem2  36266  mbfresfi  36529  pwinfi  42305  pwsal  45021  intsal  45036  salexct  45040  0ome  45235