Theorem vuniex 7738

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

Syntax hints:   ∈ wcel 2099  Vcvv 3470  ∪ cuni 4903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-sep 5293  ax-un 7734

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3472  df-uni 4904

This theorem is referenced by:  uniexg  7739  uniuni  7758  rankuni  9880  r0weon  10029  dfac3  10138  dfac5lem4  10143  dfac8  10152  dfacacn  10158  kmlem2  10168  cfslb2n  10285  ttukeylem5  10530  ttukeylem6  10531  brdom7disj  10548  brdom6disj  10549  intwun  10752  wunex2  10755  fnmrc  17580  mrcfval  17581  mrisval  17603  sylow2a  19567  toprntopon  22820  distop  22891  fctop  22900  cctop  22902  ppttop  22903  epttop  22905  fncld  22919  mretopd  22989  toponmre  22990  iscnp2  23136  2ndcsep  23356  kgenf  23438  alexsubALTlem2  23945  pwsiga  33743  sigainb  33749  dmsigagen  33757  pwldsys  33770  ldsysgenld  33773  ldgenpisyslem1  33776  ddemeas  33849  brapply  35528  dfrdg4  35541  fnessref  35835  neibastop1  35837  finxpreclem2  36863  mbfresfi  37133  pwinfi  42988  pwsal  45697  intsal  45712  salexct  45716  0ome  45911

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »