Theorem vuniex 7738

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

Syntax hints:   ∈ wcel 2149  Vcvv 3463  ∪ cuni 4876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-uni 4877

This theorem is referenced by:  uniexg  7739  uniuni  7761  rankuni  9835  r0weon  9996  dfac3  10105  dfac5lem4  10110  dfac8  10119  dfacacn  10125  kmlem2  10135  cfslb2n  10252  ttukeylem5  10497  ttukeylem6  10498  brdom7disj  10515  brdom6disj  10516  intwun  10720  wunex2  10723  fnmrc  17663  mrcfval  17664  mrisval  17686  sylow2a  19689  toprntopon  23051  distop  23121  fctop  23130  cctop  23132  ppttop  23133  epttop  23135  fncld  23148  mretopd  23218  toponmre  23219  iscnp2  23365  2ndcsep  23585  kgenf  23667  alexsubALTlem2  24174  pwsiga  34465  sigainb  34471  dmsigagen  34479  pwldsys  34492  ldsysgenld  34495  ldgenpisyslem1  34498  ddemeas  34571  brapply  36327  dfrdg4  36342  fnessref  36757  neibastop1  36759  finxpreclem2  37924  mbfresfi  38205  pwinfi  44182  pwsal  46921  intsal  46936  salexct  46940  0ome  47135