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

Theorem vuniex 7184
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 3394 . 2 𝑥 ∈ V
21uniex 7183 1 𝑥 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2156  Vcvv 3391   cuni 4630
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-un 7179
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-rex 3102  df-v 3393  df-uni 4631
This theorem is referenced by:  uniexg  7185  uniuni  7201  rankuni  8973  r0weon  9118  dfac3  9227  dfac5lem4  9232  dfac8  9242  dfacacn  9248  kmlem2  9258  cfslb2n  9375  ttukeylem5  9620  ttukeylem6  9621  brdom7disj  9638  brdom6disj  9639  intwun  9842  wunex2  9845  fnmrc  16472  mrcfval  16473  mrisval  16495  sylow2a  18235  toprntopon  20943  distop  21013  fctop  21022  cctop  21024  ppttop  21025  epttop  21027  fncld  21040  mretopd  21110  toponmre  21111  iscnp2  21257  2ndcsep  21476  kgenf  21558  alexsubALTlem2  22065  pwsiga  30518  sigainb  30524  dmsigagen  30532  pwldsys  30545  ldsysgenld  30548  ldgenpisyslem1  30551  ddemeas  30624  brapply  32366  dfrdg4  32379  fnessref  32673  neibastop1  32675  finxpreclem2  33543  mbfresfi  33768  pwinfi  38369  pwsal  41014  intsal  41027  salexct  41031  0ome  41225
  Copyright terms: Public domain W3C validator