Theorem vuniex 7733

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

Syntax hints:   ∈ wcel 2108  Vcvv 3459  ∪ cuni 4883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-un 7729

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-uni 4884

This theorem is referenced by:  uniexg  7734  uniuni  7756  rankuni  9877  r0weon  10026  dfac3  10135  dfac5lem4  10140  dfac5lem4OLD  10142  dfac8  10150  dfacacn  10156  kmlem2  10166  cfslb2n  10282  ttukeylem5  10527  ttukeylem6  10528  brdom7disj  10545  brdom6disj  10546  intwun  10749  wunex2  10752  fnmrc  17619  mrcfval  17620  mrisval  17642  sylow2a  19600  toprntopon  22863  distop  22933  fctop  22942  cctop  22944  ppttop  22945  epttop  22947  fncld  22960  mretopd  23030  toponmre  23031  iscnp2  23177  2ndcsep  23397  kgenf  23479  alexsubALTlem2  23986  pwsiga  34161  sigainb  34167  dmsigagen  34175  pwldsys  34188  ldsysgenld  34191  ldgenpisyslem1  34194  ddemeas  34267  brapply  35956  dfrdg4  35969  fnessref  36375  neibastop1  36377  finxpreclem2  37408  mbfresfi  37690  pwinfi  43588  pwsal  46344  intsal  46359  salexct  46363  0ome  46558