Theorem vuniex 7469

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

Syntax hints:   ∈ wcel 2111  Vcvv 3409  ∪ cuni 4801

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729  ax-sep 5173  ax-un 7465

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-uni 4802

This theorem is referenced by:  uniexg  7470  uniuni  7489  rankuni  9338  r0weon  9485  dfac3  9594  dfac5lem4  9599  dfac8  9608  dfacacn  9614  kmlem2  9624  cfslb2n  9741  ttukeylem5  9986  ttukeylem6  9987  brdom7disj  10004  brdom6disj  10005  intwun  10208  wunex2  10211  fnmrc  16949  mrcfval  16950  mrisval  16972  sylow2a  18824  toprntopon  21638  distop  21708  fctop  21717  cctop  21719  ppttop  21720  epttop  21722  fncld  21735  mretopd  21805  toponmre  21806  iscnp2  21952  2ndcsep  22172  kgenf  22254  alexsubALTlem2  22761  pwsiga  31629  sigainb  31635  dmsigagen  31643  pwldsys  31656  ldsysgenld  31659  ldgenpisyslem1  31662  ddemeas  31735  brapply  33823  dfrdg4  33836  fnessref  34129  neibastop1  34131  finxpreclem2  35121  mbfresfi  35417  pwinfi  40671  pwsal  43358  intsal  43371  salexct  43375  0ome  43569