Theorem vuniex 7695

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

Syntax hints:   ∈ wcel 2109  Vcvv 3444  ∪ cuni 4867

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-un 7691

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-uni 4868

This theorem is referenced by:  uniexg  7696  uniuni  7718  rankuni  9792  r0weon  9941  dfac3  10050  dfac5lem4  10055  dfac5lem4OLD  10057  dfac8  10065  dfacacn  10071  kmlem2  10081  cfslb2n  10197  ttukeylem5  10442  ttukeylem6  10443  brdom7disj  10460  brdom6disj  10461  intwun  10664  wunex2  10667  fnmrc  17544  mrcfval  17545  mrisval  17567  sylow2a  19525  toprntopon  22788  distop  22858  fctop  22867  cctop  22869  ppttop  22870  epttop  22872  fncld  22885  mretopd  22955  toponmre  22956  iscnp2  23102  2ndcsep  23322  kgenf  23404  alexsubALTlem2  23911  pwsiga  34093  sigainb  34099  dmsigagen  34107  pwldsys  34120  ldsysgenld  34123  ldgenpisyslem1  34126  ddemeas  34199  brapply  35899  dfrdg4  35912  fnessref  36318  neibastop1  36320  finxpreclem2  37351  mbfresfi  37633  pwinfi  43526  pwsal  46286  intsal  46301  salexct  46305  0ome  46500