Theorem vuniex 7672

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

Syntax hints:   ∈ wcel 2111  Vcvv 3436  ∪ cuni 4856

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-uni 4857

This theorem is referenced by:  uniexg  7673  uniuni  7695  rankuni  9756  r0weon  9903  dfac3  10012  dfac5lem4  10017  dfac5lem4OLD  10019  dfac8  10027  dfacacn  10033  kmlem2  10043  cfslb2n  10159  ttukeylem5  10404  ttukeylem6  10405  brdom7disj  10422  brdom6disj  10423  intwun  10626  wunex2  10629  fnmrc  17513  mrcfval  17514  mrisval  17536  sylow2a  19531  toprntopon  22840  distop  22910  fctop  22919  cctop  22921  ppttop  22922  epttop  22924  fncld  22937  mretopd  23007  toponmre  23008  iscnp2  23154  2ndcsep  23374  kgenf  23456  alexsubALTlem2  23963  pwsiga  34143  sigainb  34149  dmsigagen  34157  pwldsys  34170  ldsysgenld  34173  ldgenpisyslem1  34176  ddemeas  34249  brapply  35980  dfrdg4  35995  fnessref  36401  neibastop1  36403  finxpreclem2  37434  mbfresfi  37716  pwinfi  43667  pwsal  46423  intsal  46438  salexct  46442  0ome  46637