Theorem vuniex 7592

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

Syntax hints:   ∈ wcel 2106  Vcvv 3432  ∪ cuni 4839

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-uni 4840

This theorem is referenced by:  uniexg  7593  uniuni  7612  rankuni  9621  r0weon  9768  dfac3  9877  dfac5lem4  9882  dfac8  9891  dfacacn  9897  kmlem2  9907  cfslb2n  10024  ttukeylem5  10269  ttukeylem6  10270  brdom7disj  10287  brdom6disj  10288  intwun  10491  wunex2  10494  fnmrc  17316  mrcfval  17317  mrisval  17339  sylow2a  19224  toprntopon  22074  distop  22145  fctop  22154  cctop  22156  ppttop  22157  epttop  22159  fncld  22173  mretopd  22243  toponmre  22244  iscnp2  22390  2ndcsep  22610  kgenf  22692  alexsubALTlem2  23199  pwsiga  32098  sigainb  32104  dmsigagen  32112  pwldsys  32125  ldsysgenld  32128  ldgenpisyslem1  32131  ddemeas  32204  brapply  34240  dfrdg4  34253  fnessref  34546  neibastop1  34548  finxpreclem2  35561  mbfresfi  35823  pwinfi  41171  pwsal  43856  intsal  43869  salexct  43873  0ome  44067