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

Theorem vuniex 7099
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 3354 . 2 𝑥 ∈ V
21uniex 7098 1 𝑥 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2145  Vcvv 3351   cuni 4574
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-un 7094
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rex 3067  df-v 3353  df-uni 4575
This theorem is referenced by:  uniexg  7100  uniuni  7116  rankuni  8888  r0weon  9033  dfac3  9142  dfac5lem4  9147  dfac8  9157  dfacacn  9163  kmlem2  9173  cfslb2n  9290  ttukeylem5  9535  ttukeylem6  9536  brdom7disj  9553  brdom6disj  9554  intwun  9757  wunex2  9760  fnmrc  16468  mrcfval  16469  mrisval  16491  sylow2a  18234  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  30526  sigainb  30532  dmsigagen  30540  pwldsys  30553  ldsysgenld  30556  ldgenpisyslem1  30559  ddemeas  30632  brapply  32375  dfrdg4  32388  fnessref  32682  neibastop1  32684  finxpreclem2  33557  mbfresfi  33781  pwinfi  38388  pwsal  41045  intsal  41058  salexct  41062  0ome  41256
  Copyright terms: Public domain W3C validator