Theorem vuniex 7774

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

Syntax hints:   ∈ wcel 2108  Vcvv 3488  ∪ cuni 4931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-uni 4932

This theorem is referenced by:  uniexg  7775  uniuni  7797  rankuni  9932  r0weon  10081  dfac3  10190  dfac5lem4  10195  dfac5lem4OLD  10197  dfac8  10205  dfacacn  10211  kmlem2  10221  cfslb2n  10337  ttukeylem5  10582  ttukeylem6  10583  brdom7disj  10600  brdom6disj  10601  intwun  10804  wunex2  10807  fnmrc  17665  mrcfval  17666  mrisval  17688  sylow2a  19661  toprntopon  22952  distop  23023  fctop  23032  cctop  23034  ppttop  23035  epttop  23037  fncld  23051  mretopd  23121  toponmre  23122  iscnp2  23268  2ndcsep  23488  kgenf  23570  alexsubALTlem2  24077  pwsiga  34094  sigainb  34100  dmsigagen  34108  pwldsys  34121  ldsysgenld  34124  ldgenpisyslem1  34127  ddemeas  34200  brapply  35902  dfrdg4  35915  fnessref  36323  neibastop1  36325  finxpreclem2  37356  mbfresfi  37626  pwinfi  43526  pwsal  46236  intsal  46251  salexct  46255  0ome  46450