Theorem vuniex 7758

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

Syntax hints:   ∈ wcel 2106  Vcvv 3478  ∪ cuni 4912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-uni 4913

This theorem is referenced by:  uniexg  7759  uniuni  7781  rankuni  9901  r0weon  10050  dfac3  10159  dfac5lem4  10164  dfac5lem4OLD  10166  dfac8  10174  dfacacn  10180  kmlem2  10190  cfslb2n  10306  ttukeylem5  10551  ttukeylem6  10552  brdom7disj  10569  brdom6disj  10570  intwun  10773  wunex2  10776  fnmrc  17652  mrcfval  17653  mrisval  17675  sylow2a  19652  toprntopon  22947  distop  23018  fctop  23027  cctop  23029  ppttop  23030  epttop  23032  fncld  23046  mretopd  23116  toponmre  23117  iscnp2  23263  2ndcsep  23483  kgenf  23565  alexsubALTlem2  24072  pwsiga  34111  sigainb  34117  dmsigagen  34125  pwldsys  34138  ldsysgenld  34141  ldgenpisyslem1  34144  ddemeas  34217  brapply  35920  dfrdg4  35933  fnessref  36340  neibastop1  36342  finxpreclem2  37373  mbfresfi  37653  pwinfi  43554  pwsal  46271  intsal  46286  salexct  46290  0ome  46485