MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  uniexg Unicode version

Theorem uniexg 4646
Description: The ZF Axiom of Union in class notation, in the form of a theorem instead of an inference. We use the antecedent  A  e.  V instead of  A  e.  _V to make the theorem more general and thus shorten some proofs; obviously the universal class constant  _V is one possible substitution for class variable  V. (Contributed by NM, 25-Nov-1994.)
Assertion
Ref Expression
uniexg  |-  ( A  e.  V  ->  U. A  e.  _V )

Proof of Theorem uniexg
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 unieq 3966 . . 3  |-  ( x  =  A  ->  U. x  =  U. A )
21eleq1d 2453 . 2  |-  ( x  =  A  ->  ( U. x  e.  _V  <->  U. A  e.  _V )
)
3 vex 2902 . . 3  |-  x  e. 
_V
43uniex 4645 . 2  |-  U. x  e.  _V
52, 4vtoclg 2954 1  |-  ( A  e.  V  ->  U. A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1717   _Vcvv 2899   U.cuni 3957
This theorem is referenced by:  snnex  4653  uniexb  4692  ssonuni  4707  ssonprc  4712  dmexg  5070  rnexg  5071  iunexg  5926  undefval  6482  onovuni  6540  tz7.44lem1  6599  tz7.44-3  6602  en1b  7111  disjen  7200  domss2  7202  fival  7352  fipwuni  7366  supexd  7391  cantnflem1  7578  dfac8clem  7846  onssnum  7854  dfac12lem1  7956  dfac12lem2  7957  fin1a2lem12  8224  hsmexlem1  8239  axdc2lem  8261  ttukeylem3  8324  wrdexb  11690  restid  13588  prdsbas  13607  prdsplusg  13608  prdsmulr  13609  prdsvsca  13610  prdshom  13616  sscpwex  13942  frgpcyg  16777  eltopspOLD  16906  istpsOLD  16908  istopon  16913  tgval  16943  eltg  16945  eltg2  16946  tgss2  16975  ntrval  17023  neiptoptop  17118  neiptopnei  17119  restin  17152  neitr  17166  restntr  17168  cnpresti  17274  cnprest  17275  cnprest2  17276  lmcnp  17290  pnrmopn  17329  cnrmnrm  17347  cmpsublem  17384  cmpsub  17385  cmpcld  17387  hausmapdom  17484  txbasex  17519  dfac14lem  17570  uptx  17578  xkopt  17608  xkopjcn  17609  qtopval2  17649  elqtop  17650  fbssfi  17790  ptcmplem2  18005  cnextfval  18014  cnextcn  18019  tuslem  18218  isppw  20764  hasheuni  24271  insiga  24316  sigagenval  24319  braew  24387  isrrvv  24480  rrvmulc  24490  kur14  24681  cvmscld  24739  relexp0  24908  relexpsucr  24909  nobndlem1  25370  fobigcup  25464  hfuni  25839  isfne  26039  isfne4b  26041  isref  26050  locfindis  26076  topjoin  26085  fnemeet1  26086  tailfval  26092  supex2g  26130  kelac2  26832  en1uniel  27049  pmtrfv  27064  cnfex  27367  stoweidlem50  27467  stoweidlem57  27474  stoweidlem59  27476  stoweidlem60  27477  bnj1489  28763
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271  ax-un 4641
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-rex 2655  df-v 2901  df-uni 3958
  Copyright terms: Public domain W3C validator