Theorem vuniex 7684

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

Syntax hints:   ∈ wcel 2113  Vcvv 3440  ∪ cuni 4863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-uni 4864

This theorem is referenced by:  uniexg  7685  uniuni  7707  rankuni  9775  r0weon  9922  dfac3  10031  dfac5lem4  10036  dfac5lem4OLD  10038  dfac8  10046  dfacacn  10052  kmlem2  10062  cfslb2n  10178  ttukeylem5  10423  ttukeylem6  10424  brdom7disj  10441  brdom6disj  10442  intwun  10646  wunex2  10649  fnmrc  17530  mrcfval  17531  mrisval  17553  sylow2a  19548  toprntopon  22869  distop  22939  fctop  22948  cctop  22950  ppttop  22951  epttop  22953  fncld  22966  mretopd  23036  toponmre  23037  iscnp2  23183  2ndcsep  23403  kgenf  23485  alexsubALTlem2  23992  pwsiga  34287  sigainb  34293  dmsigagen  34301  pwldsys  34314  ldsysgenld  34317  ldgenpisyslem1  34320  ddemeas  34393  brapply  36130  dfrdg4  36145  fnessref  36551  neibastop1  36553  finxpreclem2  37595  mbfresfi  37867  pwinfi  43805  pwsal  46559  intsal  46574  salexct  46578  0ome  46773