Theorem vuniex 7694

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

Syntax hints:   ∈ wcel 2114  Vcvv 3442  ∪ cuni 4865

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 5243  ax-un 7690

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 3444  df-uni 4866

This theorem is referenced by:  uniexg  7695  uniuni  7717  rankuni  9787  r0weon  9934  dfac3  10043  dfac5lem4  10048  dfac5lem4OLD  10050  dfac8  10058  dfacacn  10064  kmlem2  10074  cfslb2n  10190  ttukeylem5  10435  ttukeylem6  10436  brdom7disj  10453  brdom6disj  10454  intwun  10658  wunex2  10661  fnmrc  17542  mrcfval  17543  mrisval  17565  sylow2a  19560  toprntopon  22881  distop  22951  fctop  22960  cctop  22962  ppttop  22963  epttop  22965  fncld  22978  mretopd  23048  toponmre  23049  iscnp2  23195  2ndcsep  23415  kgenf  23497  alexsubALTlem2  24004  pwsiga  34308  sigainb  34314  dmsigagen  34322  pwldsys  34335  ldsysgenld  34338  ldgenpisyslem1  34341  ddemeas  34414  brapply  36152  dfrdg4  36167  fnessref  36573  neibastop1  36575  finxpreclem2  37645  mbfresfi  37917  pwinfi  43920  pwsal  46673  intsal  46688  salexct  46692  0ome  46887