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 3473	1 ⊢ ∪ 𝑥 ∈ V

Syntax hints:   ∈ wcel 2142  Vcvv 3454  ∪ cuni 4865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-uni 4866

This theorem is referenced by:  uniexg  7723  uniuni  7745  rankuni  9821  r0weon  9968  dfac3  10077  dfac5lem4  10082  dfac5lem4OLD  10084  dfac8  10092  dfacacn  10098  kmlem2  10108  cfslb2n  10225  ttukeylem5  10470  ttukeylem6  10471  brdom7disj  10488  brdom6disj  10489  intwun  10693  wunex2  10696  fnmrc  17639  mrcfval  17640  mrisval  17662  sylow2a  19659  toprntopon  22985  distop  23055  fctop  23064  cctop  23066  ppttop  23067  epttop  23069  fncld  23082  mretopd  23152  toponmre  23153  iscnp2  23299  2ndcsep  23519  kgenf  23601  alexsubALTlem2  24108  pwsiga  34427  sigainb  34433  dmsigagen  34441  pwldsys  34454  ldsysgenld  34457  ldgenpisyslem1  34460  ddemeas  34533  brapply  36286  dfrdg4  36301  fnessref  36717  neibastop1  36719  finxpreclem2  37884  mbfresfi  38165  pwinfi  44140  pwsal  46889  intsal  46904  salexct  46908  0ome  47103