Theorem vuniex 7756

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451  ∪ cuni 4867

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-uni 4868

This theorem is used by:  uniexg  7757  uniuni  7776  rankuni  9879  r0weon  10091  dfac3  10200  dfac5lem4  10205  dfac8  10214  dfacacn  10220  kmlem2  10230  cfslb2n  10346  ttukeylem5  10591  ttukeylem6  10592  brdom7disj  10610  brdom6disj  10611  intwun  10820  wunex2  10823  fnmrc  17781  mrcfval  17782  mrisval  17804  sylow2a  19833  toprntopon  23243  distop  23313  fctop  23322  cctop  23324  ppttop  23325  epttop  23327  fncld  23340  mretopd  23410  toponmre  23411  iscnp2  23557  2ndcsep  23778  kgenf  23860  alexsubALTlem2  24367  pwsiga  34762  sigainb  34769  dmsigagen  34777  pwldsys  34790  ldsysgenld  34793  ldgenpisyslem1  34796  ddemeas  34869  brapply  36700  dfrdg4  36715  fnessref  37145  neibastop1  37147  finxpreclem2  38313  mbfresfi  38584  pwinfi  44564  pwsal  47324  intsal  47339  salexct  47343  0ome  47538