Theorem vuniex 7737

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

Syntax hints:   ∈ wcel 2143  Vcvv 3455  ∪ cuni 4872

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-uni 4873

This theorem is referenced by:  uniexg  7738  uniuni  7757  rankuni  9831  r0weon  9992  dfac3  10101  dfac5lem4  10106  dfac8  10115  dfacacn  10121  kmlem2  10131  cfslb2n  10247  ttukeylem5  10492  ttukeylem6  10493  brdom7disj  10510  brdom6disj  10511  intwun  10715  wunex2  10718  fnmrc  17658  mrcfval  17659  mrisval  17681  sylow2a  19684  toprntopon  23082  distop  23152  fctop  23161  cctop  23163  ppttop  23164  epttop  23166  fncld  23179  mretopd  23249  toponmre  23250  iscnp2  23396  2ndcsep  23616  kgenf  23698  alexsubALTlem2  24205  pwsiga  34520  sigainb  34526  dmsigagen  34534  pwldsys  34547  ldsysgenld  34550  ldgenpisyslem1  34553  ddemeas  34626  brapply  36428  dfrdg4  36443  fnessref  36888  neibastop1  36890  finxpreclem2  38056  mbfresfi  38337  pwinfi  44310  pwsal  47049  intsal  47064  salexct  47068  0ome  47263