Theorem vuniex 7570

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

Syntax hints:   ∈ wcel 2108  Vcvv 3422  ∪ cuni 4836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-uni 4837

This theorem is referenced by:  uniexg  7571  uniuni  7590  rankuni  9552  r0weon  9699  dfac3  9808  dfac5lem4  9813  dfac8  9822  dfacacn  9828  kmlem2  9838  cfslb2n  9955  ttukeylem5  10200  ttukeylem6  10201  brdom7disj  10218  brdom6disj  10219  intwun  10422  wunex2  10425  fnmrc  17233  mrcfval  17234  mrisval  17256  sylow2a  19139  toprntopon  21982  distop  22053  fctop  22062  cctop  22064  ppttop  22065  epttop  22067  fncld  22081  mretopd  22151  toponmre  22152  iscnp2  22298  2ndcsep  22518  kgenf  22600  alexsubALTlem2  23107  pwsiga  31998  sigainb  32004  dmsigagen  32012  pwldsys  32025  ldsysgenld  32028  ldgenpisyslem1  32031  ddemeas  32104  brapply  34167  dfrdg4  34180  fnessref  34473  neibastop1  34475  finxpreclem2  35488  mbfresfi  35750  pwinfi  41060  pwsal  43746  intsal  43759  salexct  43763  0ome  43957