Theorem vuniex 7722

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

Syntax hints:   ∈ wcel 2098  Vcvv 3466  ∪ cuni 4899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695  ax-sep 5289  ax-un 7718

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468  df-uni 4900

This theorem is referenced by:  uniexg  7723  uniuni  7742  rankuni  9854  r0weon  10003  dfac3  10112  dfac5lem4  10117  dfac8  10126  dfacacn  10132  kmlem2  10142  cfslb2n  10259  ttukeylem5  10504  ttukeylem6  10505  brdom7disj  10522  brdom6disj  10523  intwun  10726  wunex2  10729  fnmrc  17550  mrcfval  17551  mrisval  17573  sylow2a  19529  toprntopon  22749  distop  22820  fctop  22829  cctop  22831  ppttop  22832  epttop  22834  fncld  22848  mretopd  22918  toponmre  22919  iscnp2  23065  2ndcsep  23285  kgenf  23367  alexsubALTlem2  23874  pwsiga  33617  sigainb  33623  dmsigagen  33631  pwldsys  33644  ldsysgenld  33647  ldgenpisyslem1  33650  ddemeas  33723  brapply  35405  dfrdg4  35418  fnessref  35732  neibastop1  35734  finxpreclem2  36761  mbfresfi  37024  pwinfi  42804  pwsal  45516  intsal  45531  salexct  45535  0ome  45730