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  33128  sigainb  33134  dmsigagen  33142  pwldsys  33155  ldsysgenld  33158  ldgenpisyslem1  33161  ddemeas  33234  brapply  34910  dfrdg4  34923  fnessref  35242  neibastop1  35244  finxpreclem2  36271  mbfresfi  36534  pwinfi  42315  pwsal  45031  intsal  45046  salexct  45050  0ome  45245