Theorem vuniex 7747

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

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3457  ∪ cuni 4874

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 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-un 7742

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-uni 4875

This theorem is used by:  uniexg  7748  uniuni  7767  rankuni  9842  r0weon  10012  dfac3  10121  dfac5lem4  10126  dfac8  10135  dfacacn  10141  kmlem2  10151  cfslb2n  10267  ttukeylem5  10512  ttukeylem6  10513  brdom7disj  10530  brdom6disj  10531  intwun  10737  wunex2  10740  fnmrc  17687  mrcfval  17688  mrisval  17710  sylow2a  19735  toprntopon  23134  distop  23204  fctop  23213  cctop  23215  ppttop  23216  epttop  23218  fncld  23231  mretopd  23301  toponmre  23302  iscnp2  23448  2ndcsep  23669  kgenf  23751  alexsubALTlem2  24258  pwsiga  34586  sigainb  34593  dmsigagen  34601  pwldsys  34614  ldsysgenld  34617  ldgenpisyslem1  34620  ddemeas  34693  brapply  36467  dfrdg4  36482  fnessref  36927  neibastop1  36929  finxpreclem2  38095  mbfresfi  38376  pwinfi  44350  pwsal  47089  intsal  47104  salexct  47108  0ome  47303