Theorem vuniex 7695

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

Syntax hints:   ∈ wcel 2109  Vcvv 3444  ∪ cuni 4867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-un 7691

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-uni 4868

This theorem is referenced by:  uniexg  7696  uniuni  7718  rankuni  9792  r0weon  9941  dfac3  10050  dfac5lem4  10055  dfac5lem4OLD  10057  dfac8  10065  dfacacn  10071  kmlem2  10081  cfslb2n  10197  ttukeylem5  10442  ttukeylem6  10443  brdom7disj  10460  brdom6disj  10461  intwun  10664  wunex2  10667  fnmrc  17548  mrcfval  17549  mrisval  17571  sylow2a  19533  toprntopon  22845  distop  22915  fctop  22924  cctop  22926  ppttop  22927  epttop  22929  fncld  22942  mretopd  23012  toponmre  23013  iscnp2  23159  2ndcsep  23379  kgenf  23461  alexsubALTlem2  23968  pwsiga  34113  sigainb  34119  dmsigagen  34127  pwldsys  34140  ldsysgenld  34143  ldgenpisyslem1  34146  ddemeas  34219  brapply  35919  dfrdg4  35932  fnessref  36338  neibastop1  36340  finxpreclem2  37371  mbfresfi  37653  pwinfi  43546  pwsal  46306  intsal  46321  salexct  46325  0ome  46520