Theorem vuniex 7759

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

Syntax hints:   ∈ wcel 2108  Vcvv 3480  ∪ cuni 4907

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 2708  ax-sep 5296  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-uni 4908

This theorem is referenced by:  uniexg  7760  uniuni  7782  rankuni  9903  r0weon  10052  dfac3  10161  dfac5lem4  10166  dfac5lem4OLD  10168  dfac8  10176  dfacacn  10182  kmlem2  10192  cfslb2n  10308  ttukeylem5  10553  ttukeylem6  10554  brdom7disj  10571  brdom6disj  10572  intwun  10775  wunex2  10778  fnmrc  17650  mrcfval  17651  mrisval  17673  sylow2a  19637  toprntopon  22931  distop  23002  fctop  23011  cctop  23013  ppttop  23014  epttop  23016  fncld  23030  mretopd  23100  toponmre  23101  iscnp2  23247  2ndcsep  23467  kgenf  23549  alexsubALTlem2  24056  pwsiga  34131  sigainb  34137  dmsigagen  34145  pwldsys  34158  ldsysgenld  34161  ldgenpisyslem1  34164  ddemeas  34237  brapply  35939  dfrdg4  35952  fnessref  36358  neibastop1  36360  finxpreclem2  37391  mbfresfi  37673  pwinfi  43577  pwsal  46330  intsal  46345  salexct  46349  0ome  46544