Theorem vuniex 7467

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

Syntax hints:   ∈ wcel 2114  Vcvv 3496  ∪ cuni 4840

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-un 7463

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-uni 4841

This theorem is referenced by:  uniexg  7468  uniuni  7486  rankuni  9294  r0weon  9440  dfac3  9549  dfac5lem4  9554  dfac8  9563  dfacacn  9569  kmlem2  9579  cfslb2n  9692  ttukeylem5  9937  ttukeylem6  9938  brdom7disj  9955  brdom6disj  9956  intwun  10159  wunex2  10162  fnmrc  16880  mrcfval  16881  mrisval  16903  sylow2a  18746  toprntopon  21535  distop  21605  fctop  21614  cctop  21616  ppttop  21617  epttop  21619  fncld  21632  mretopd  21702  toponmre  21703  iscnp2  21849  2ndcsep  22069  kgenf  22151  alexsubALTlem2  22658  pwsiga  31391  sigainb  31397  dmsigagen  31405  pwldsys  31418  ldsysgenld  31421  ldgenpisyslem1  31424  ddemeas  31497  brapply  33401  dfrdg4  33414  fnessref  33707  neibastop1  33709  finxpreclem2  34673  mbfresfi  34940  pwinfi  39930  pwsal  42607  intsal  42620  salexct  42624  0ome  42818