Theorem vuniex 7715

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

Syntax hints:   ∈ wcel 2109  Vcvv 3447  ∪ cuni 4871

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 5251  ax-un 7711

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 3449  df-uni 4872

This theorem is referenced by:  uniexg  7716  uniuni  7738  rankuni  9816  r0weon  9965  dfac3  10074  dfac5lem4  10079  dfac5lem4OLD  10081  dfac8  10089  dfacacn  10095  kmlem2  10105  cfslb2n  10221  ttukeylem5  10466  ttukeylem6  10467  brdom7disj  10484  brdom6disj  10485  intwun  10688  wunex2  10691  fnmrc  17568  mrcfval  17569  mrisval  17591  sylow2a  19549  toprntopon  22812  distop  22882  fctop  22891  cctop  22893  ppttop  22894  epttop  22896  fncld  22909  mretopd  22979  toponmre  22980  iscnp2  23126  2ndcsep  23346  kgenf  23428  alexsubALTlem2  23935  pwsiga  34120  sigainb  34126  dmsigagen  34134  pwldsys  34147  ldsysgenld  34150  ldgenpisyslem1  34153  ddemeas  34226  brapply  35926  dfrdg4  35939  fnessref  36345  neibastop1  36347  finxpreclem2  37378  mbfresfi  37660  pwinfi  43553  pwsal  46313  intsal  46328  salexct  46332  0ome  46527