MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  vuniex Structured version   Visualization version   GIF version

Theorem vuniex 6907
Description: The union of a setvar is a set. (Contributed by BJ, 3-May-2021.)
Assertion
Ref Expression
vuniex 𝑥 ∈ V

Proof of Theorem vuniex
StepHypRef Expression
1 vex 3189 . 2 𝑥 ∈ V
21uniex 6906 1 𝑥 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 1987  Vcvv 3186   cuni 4402
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rex 2913  df-v 3188  df-uni 4403
This theorem is referenced by:  uniexg  6908  uniuni  6920  rankuni  8670  r0weon  8779  dfac3  8888  dfac5lem4  8893  dfac8  8901  dfacacn  8907  kmlem2  8917  cfslb2n  9034  ttukeylem5  9279  ttukeylem6  9280  brdom7disj  9297  brdom6disj  9298  intwun  9501  wunex2  9504  fnmrc  16188  mrcfval  16189  mrisval  16211  sylow2a  17955  distop  20710  fctop  20718  cctop  20720  ppttop  20721  epttop  20723  fncld  20736  mretopd  20806  toponmre  20807  iscnp2  20953  2ndcsep  21172  kgenf  21254  alexsubALTlem2  21762  pwsiga  29974  sigainb  29980  dmsigagen  29988  pwldsys  30001  ldsysgenld  30004  ldgenpisyslem1  30007  ddemeas  30080  brapply  31687  dfrdg4  31700  fnessref  31994  neibastop1  31996  bj-toprntopon  32700  finxpreclem2  32859  mbfresfi  33088  pwinfi  37350  pwsal  39842  intsal  39855  salexct  39859  0ome  40050
  Copyright terms: Public domain W3C validator