Theorem vuniex 7742

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3450  ∪ cuni 4867

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-un 7737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-uni 4868

This theorem is used by:  uniexg  7743  uniuni  7762  rankuni  9846  r0weon  10016  dfac3  10125  dfac5lem4  10130  dfac8  10139  dfacacn  10145  kmlem2  10155  cfslb2n  10271  ttukeylem5  10516  ttukeylem6  10517  brdom7disj  10535  brdom6disj  10536  intwun  10745  wunex2  10748  fnmrc  17696  mrcfval  17697  mrisval  17719  sylow2a  19747  toprntopon  23151  distop  23221  fctop  23230  cctop  23232  ppttop  23233  epttop  23235  fncld  23248  mretopd  23318  toponmre  23319  iscnp2  23465  2ndcsep  23686  kgenf  23768  alexsubALTlem2  24275  pwsiga  34641  sigainb  34648  dmsigagen  34656  pwldsys  34669  ldsysgenld  34672  ldgenpisyslem1  34675  ddemeas  34748  brapply  36516  dfrdg4  36531  fnessref  36977  neibastop1  36979  finxpreclem2  38145  mbfresfi  38416  pwinfi  44405  pwsal  47144  intsal  47159  salexct  47163  0ome  47358