Theorem vuniex 7693

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

Syntax hints:   ∈ wcel 2114  Vcvv 3429  ∪ cuni 4850

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 2708  ax-sep 5231  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-uni 4851

This theorem is referenced by:  uniexg  7694  uniuni  7716  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  17573  mrcfval  17574  mrisval  17596  sylow2a  19594  toprntopon  22890  distop  22960  fctop  22969  cctop  22971  ppttop  22972  epttop  22974  fncld  22987  mretopd  23057  toponmre  23058  iscnp2  23204  2ndcsep  23424  kgenf  23506  alexsubALTlem2  24013  pwsiga  34274  sigainb  34280  dmsigagen  34288  pwldsys  34301  ldsysgenld  34304  ldgenpisyslem1  34307  ddemeas  34380  brapply  36118  dfrdg4  36133  fnessref  36539  neibastop1  36541  finxpreclem2  37706  mbfresfi  37987  pwinfi  43991  pwsal  46743  intsal  46758  salexct  46762  0ome  46957