Theorem vuniex 7760

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

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450  ∪ cuni 4866

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-un 7755

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-uni 4867

This theorem is used by:  uniexg  7761  uniuni  7780  rankuni  9886  r0weon  10098  dfac3  10207  dfac5lem4  10212  dfac8  10221  dfacacn  10227  kmlem2  10237  cfslb2n  10353  ttukeylem5  10598  ttukeylem6  10599  brdom7disj  10617  brdom6disj  10618  intwun  10827  wunex2  10830  fnmrc  17790  mrcfval  17791  mrisval  17813  sylow2a  19842  toprntopon  23252  distop  23322  fctop  23331  cctop  23333  ppttop  23334  epttop  23336  fncld  23349  mretopd  23419  toponmre  23420  iscnp2  23566  2ndcsep  23787  kgenf  23869  alexsubALTlem2  24376  pwsiga  34812  sigainb  34819  dmsigagen  34827  pwldsys  34840  ldsysgenld  34843  ldgenpisyslem1  34846  ddemeas  34919  brapply  36824  dfrdg4  36839  fnessref  37269  neibastop1  37271  finxpreclem2  38450  mbfresfi  38721  pwinfi  44702  pwsal  47461  intsal  47476  salexct  47480  0ome  47675