Theorem vuniex 7682

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

Syntax hints:   ∈ wcel 2119  Vcvv 3431  ∪ cuni 4838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-uni 4839

This theorem is referenced by:  uniexg  7683  uniuni  7705  rankuni  9778  r0weon  9925  dfac3  10034  dfac5lem4  10039  dfac5lem4OLD  10041  dfac8  10049  dfacacn  10055  kmlem2  10065  cfslb2n  10181  ttukeylem5  10426  ttukeylem6  10427  brdom7disj  10444  brdom6disj  10445  intwun  10649  wunex2  10652  fnmrc  17564  mrcfval  17565  mrisval  17587  sylow2a  19585  toprntopon  22908  distop  22978  fctop  22987  cctop  22989  ppttop  22990  epttop  22992  fncld  23005  mretopd  23075  toponmre  23076  iscnp2  23222  2ndcsep  23442  kgenf  23524  alexsubALTlem2  24031  pwsiga  34314  sigainb  34320  dmsigagen  34328  pwldsys  34341  ldsysgenld  34344  ldgenpisyslem1  34347  ddemeas  34420  brapply  36164  dfrdg4  36179  fnessref  36585  neibastop1  36587  finxpreclem2  37752  mbfresfi  38033  pwinfi  44008  pwsal  46758  intsal  46773  salexct  46777  0ome  46972