Theorem vuniex 6852

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

Syntax hints:   ∈ wcel 1977  Vcvv 3173  ∪ cuni 4372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-v 3175  df-uni 4373

This theorem is referenced by:  uniexg  6853  uniuni  6865  rankuni  8609  r0weon  8718  dfac3  8827  dfac5lem4  8832  dfac8  8840  dfacacn  8846  kmlem2  8856  cfslb2n  8973  ttukeylem5  9218  ttukeylem6  9219  brdom7disj  9234  brdom6disj  9235  intwun  9436  wunex2  9439  fnmrc  16090  mrcfval  16091  mrisval  16113  sylow2a  17857  distop  20610  fctop  20618  cctop  20620  ppttop  20621  epttop  20623  fncld  20636  mretopd  20706  toponmre  20707  iscnp2  20853  2ndcsep  21072  kgenf  21154  alexsubALTlem2  21662  pwsiga  29520  sigainb  29526  dmsigagen  29534  pwldsys  29547  ldsysgenld  29550  ldgenpisyslem1  29553  ddemeas  29626  brapply  31215  dfrdg4  31228  fnessref  31522  neibastop1  31524  bj-toprntopon  32244  finxpreclem2  32403  mbfresfi  32626  pwinfi  36888  pwsal  39211  intsal  39224  salexct  39228  0ome  39419