Theorem vuniex 7788

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

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454  ∪ cuni 4872

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-un 7783

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-uni 4873

This theorem is used by:  uniexg  7789  uniuni  7808  rankuni  9916  r0weon  10130  dfac3  10239  dfac5lem4  10244  dfac8  10253  dfacacn  10259  kmlem2  10269  cfslb2n  10385  ttukeylem5  10630  ttukeylem6  10631  brdom7disj  10649  brdom6disj  10650  intwun  10859  wunex2  10862  fnmrc  17831  mrcfval  17832  mrisval  17854  sylow2a  19884  toprntopon  23298  distop  23368  fctop  23377  cctop  23379  ppttop  23380  epttop  23382  fncld  23395  mretopd  23465  toponmre  23466  iscnp2  23612  2ndcsep  23833  kgenf  23915  alexsubALTlem2  24422  pwsiga  34873  sigainb  34880  dmsigagen  34888  pwldsys  34901  ldsysgenld  34904  ldgenpisyslem1  34907  ddemeas  34980  brapply  36915  dfrdg4  36930  fnessref  37360  neibastop1  37362  finxpreclem2  38581  mbfresfi  38852  pwinfi  44826  pwsal  47598  intsal  47613  salexct  47617  0ome  47812