Theorem vuniex 7324

Description: The union of a setvar is a set. (Contributed by BJ, 3-May-2021.)

Assertion

Ref	Expression
vuniex	⊢ ∪ 𝑥 ∈ V

Proof of Theorem vuniex

Step	Hyp	Ref	Expression
1		vex 3440	. 2 ⊢ 𝑥 ∈ V
2	1	uniex 7323	1 ⊢ ∪ 𝑥 ∈ V

Syntax hints:   ∈ wcel 2081  Vcvv 3437  ∪ cuni 4745

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769  ax-sep 5094  ax-un 7319

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-rex 3111  df-v 3439  df-uni 4746

This theorem is referenced by:  uniexg  7325  uniuni  7341  rankuni  9138  r0weon  9284  dfac3  9393  dfac5lem4  9398  dfac8  9407  dfacacn  9413  kmlem2  9423  cfslb2n  9536  ttukeylem5  9781  ttukeylem6  9782  brdom7disj  9799  brdom6disj  9800  intwun  10003  wunex2  10006  fnmrc  16707  mrcfval  16708  mrisval  16730  sylow2a  18474  toprntopon  21217  distop  21287  fctop  21296  cctop  21298  ppttop  21299  epttop  21301  fncld  21314  mretopd  21384  toponmre  21385  iscnp2  21531  2ndcsep  21751  kgenf  21833  alexsubALTlem2  22340  pwsiga  31006  sigainb  31012  dmsigagen  31020  pwldsys  31033  ldsysgenld  31036  ldgenpisyslem1  31039  ddemeas  31112  brapply  33009  dfrdg4  33022  fnessref  33315  neibastop1  33317  finxpreclem2  34221  mbfresfi  34488  pwinfi  39427  pwsal  42162  intsal  42175  salexct  42179  0ome  42373