Theorem vuniex 7686

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

Syntax hints:   ∈ wcel 2114  Vcvv 3430  ∪ cuni 4851

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 2709  ax-sep 5231  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-uni 4852

This theorem is referenced by:  uniexg  7687  uniuni  7709  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  22900  distop  22970  fctop  22979  cctop  22981  ppttop  22982  epttop  22984  fncld  22997  mretopd  23067  toponmre  23068  iscnp2  23214  2ndcsep  23434  kgenf  23516  alexsubALTlem2  24023  pwsiga  34290  sigainb  34296  dmsigagen  34304  pwldsys  34317  ldsysgenld  34320  ldgenpisyslem1  34323  ddemeas  34396  brapply  36134  dfrdg4  36149  fnessref  36555  neibastop1  36557  finxpreclem2  37720  mbfresfi  38001  pwinfi  44009  pwsal  46761  intsal  46776  salexct  46780  0ome  46975