Theorem vuniex 7729

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

Syntax hints:   ∈ wcel 2107  Vcvv 3475  ∪ cuni 4909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-un 7725

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-uni 4910

This theorem is referenced by:  uniexg  7730  uniuni  7749  rankuni  9858  r0weon  10007  dfac3  10116  dfac5lem4  10121  dfac8  10130  dfacacn  10136  kmlem2  10146  cfslb2n  10263  ttukeylem5  10508  ttukeylem6  10509  brdom7disj  10526  brdom6disj  10527  intwun  10730  wunex2  10733  fnmrc  17551  mrcfval  17552  mrisval  17574  sylow2a  19487  toprntopon  22427  distop  22498  fctop  22507  cctop  22509  ppttop  22510  epttop  22512  fncld  22526  mretopd  22596  toponmre  22597  iscnp2  22743  2ndcsep  22963  kgenf  23045  alexsubALTlem2  23552  pwsiga  33159  sigainb  33165  dmsigagen  33173  pwldsys  33186  ldsysgenld  33189  ldgenpisyslem1  33192  ddemeas  33265  brapply  34941  dfrdg4  34954  fnessref  35290  neibastop1  35292  finxpreclem2  36319  mbfresfi  36582  pwinfi  42363  pwsal  45079  intsal  45094  salexct  45098  0ome  45293