Theorem vuniex 7687

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

Syntax hints:   ∈ wcel 2114  Vcvv 3430  ∪ cuni 4851

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232  ax-un 7683

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-uni 4852

This theorem is referenced by:  uniexg  7688  uniuni  7710  rankuni  9781  r0weon  9928  dfac3  10037  dfac5lem4  10042  dfac5lem4OLD  10044  dfac8  10052  dfacacn  10058  kmlem2  10068  cfslb2n  10184  ttukeylem5  10429  ttukeylem6  10430  brdom7disj  10447  brdom6disj  10448  intwun  10652  wunex2  10655  fnmrc  17567  mrcfval  17568  mrisval  17590  sylow2a  19588  toprntopon  22903  distop  22973  fctop  22982  cctop  22984  ppttop  22985  epttop  22987  fncld  23000  mretopd  23070  toponmre  23071  iscnp2  23217  2ndcsep  23437  kgenf  23519  alexsubALTlem2  24026  pwsiga  34293  sigainb  34299  dmsigagen  34307  pwldsys  34320  ldsysgenld  34323  ldgenpisyslem1  34326  ddemeas  34399  brapply  36137  dfrdg4  36152  fnessref  36558  neibastop1  36560  finxpreclem2  37723  mbfresfi  38004  pwinfi  44012  pwsal  46764  intsal  46779  salexct  46783  0ome  46978