Theorem vuniex 7459

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

Syntax hints:   ∈ wcel 2110  Vcvv 3494  ∪ cuni 4831

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-un 7455

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-uni 4832

This theorem is referenced by:  uniexg  7460  uniuni  7478  rankuni  9286  r0weon  9432  dfac3  9541  dfac5lem4  9546  dfac8  9555  dfacacn  9561  kmlem2  9571  cfslb2n  9684  ttukeylem5  9929  ttukeylem6  9930  brdom7disj  9947  brdom6disj  9948  intwun  10151  wunex2  10154  fnmrc  16872  mrcfval  16873  mrisval  16895  sylow2a  18738  toprntopon  21527  distop  21597  fctop  21606  cctop  21608  ppttop  21609  epttop  21611  fncld  21624  mretopd  21694  toponmre  21695  iscnp2  21841  2ndcsep  22061  kgenf  22143  alexsubALTlem2  22650  pwsiga  31384  sigainb  31390  dmsigagen  31398  pwldsys  31411  ldsysgenld  31414  ldgenpisyslem1  31417  ddemeas  31490  brapply  33394  dfrdg4  33407  fnessref  33700  neibastop1  33702  finxpreclem2  34665  mbfresfi  34932  pwinfi  39916  pwsal  42594  intsal  42607  salexct  42611  0ome  42805