Theorem vuniex 6954

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 3203	. 2 ⊢ 𝑥 ∈ V
2	1	uniex 6953	1 ⊢ ∪ 𝑥 ∈ V

Syntax hints:   ∈ wcel 1990  Vcvv 3200  ∪ cuni 4436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-v 3202  df-uni 4437

This theorem is referenced by:  uniexg  6955  uniuni  6971  rankuni  8726  r0weon  8835  dfac3  8944  dfac5lem4  8949  dfac8  8957  dfacacn  8963  kmlem2  8973  cfslb2n  9090  ttukeylem5  9335  ttukeylem6  9336  brdom7disj  9353  brdom6disj  9354  intwun  9557  wunex2  9560  fnmrc  16267  mrcfval  16268  mrisval  16290  sylow2a  18034  toprntopon  20729  distop  20799  fctop  20808  cctop  20810  ppttop  20811  epttop  20813  fncld  20826  mretopd  20896  toponmre  20897  iscnp2  21043  2ndcsep  21262  kgenf  21344  alexsubALTlem2  21852  pwsiga  30193  sigainb  30199  dmsigagen  30207  pwldsys  30220  ldsysgenld  30223  ldgenpisyslem1  30226  ddemeas  30299  brapply  32045  dfrdg4  32058  fnessref  32352  neibastop1  32354  finxpreclem2  33227  mbfresfi  33456  pwinfi  37869  pwsal  40535  intsal  40548  salexct  40552  0ome  40743