Theorem vuniex 7675

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

Syntax hints:   ∈ wcel 2109  Vcvv 3436  ∪ cuni 4858

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 5235  ax-un 7671

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 3438  df-uni 4859

This theorem is referenced by:  uniexg  7676  uniuni  7698  rankuni  9759  r0weon  9906  dfac3  10015  dfac5lem4  10020  dfac5lem4OLD  10022  dfac8  10030  dfacacn  10036  kmlem2  10046  cfslb2n  10162  ttukeylem5  10407  ttukeylem6  10408  brdom7disj  10425  brdom6disj  10426  intwun  10629  wunex2  10632  fnmrc  17513  mrcfval  17514  mrisval  17536  sylow2a  19498  toprntopon  22810  distop  22880  fctop  22889  cctop  22891  ppttop  22892  epttop  22894  fncld  22907  mretopd  22977  toponmre  22978  iscnp2  23124  2ndcsep  23344  kgenf  23426  alexsubALTlem2  23933  pwsiga  34097  sigainb  34103  dmsigagen  34111  pwldsys  34124  ldsysgenld  34127  ldgenpisyslem1  34130  ddemeas  34203  brapply  35916  dfrdg4  35929  fnessref  36335  neibastop1  36337  finxpreclem2  37368  mbfresfi  37650  pwinfi  43541  pwsal  46300  intsal  46315  salexct  46319  0ome  46514