Theorem vuniex 7718

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

Syntax hints:   ∈ wcel 2109  Vcvv 3450  ∪ cuni 4874

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 2702  ax-sep 5254  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-uni 4875

This theorem is referenced by:  uniexg  7719  uniuni  7741  rankuni  9823  r0weon  9972  dfac3  10081  dfac5lem4  10086  dfac5lem4OLD  10088  dfac8  10096  dfacacn  10102  kmlem2  10112  cfslb2n  10228  ttukeylem5  10473  ttukeylem6  10474  brdom7disj  10491  brdom6disj  10492  intwun  10695  wunex2  10698  fnmrc  17575  mrcfval  17576  mrisval  17598  sylow2a  19556  toprntopon  22819  distop  22889  fctop  22898  cctop  22900  ppttop  22901  epttop  22903  fncld  22916  mretopd  22986  toponmre  22987  iscnp2  23133  2ndcsep  23353  kgenf  23435  alexsubALTlem2  23942  pwsiga  34127  sigainb  34133  dmsigagen  34141  pwldsys  34154  ldsysgenld  34157  ldgenpisyslem1  34160  ddemeas  34233  brapply  35933  dfrdg4  35946  fnessref  36352  neibastop1  36354  finxpreclem2  37385  mbfresfi  37667  pwinfi  43560  pwsal  46320  intsal  46335  salexct  46339  0ome  46534