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

Theorem uniexg 4517
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 3836 . . 3  |-  ( x  =  A  ->  U. x  =  U. A )
21eleq1d 2349 . 2  |-  ( x  =  A  ->  ( U. x  e.  _V  <->  U. A  e.  _V )
)
3 vex 2791 . . 3  |-  x  e. 
_V
43uniex 4516 . 2  |-  U. x  e.  _V
52, 4vtoclg 2843 1  |-  ( A  e.  V  ->  U. A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684   _Vcvv 2788   U.cuni 3827
This theorem is referenced by:  snnex  4524  uniexb  4563  ssonuni  4578  ssonprc  4583  dmexg  4939  rnexg  4940  iunexg  5767  undefval  6301  onovuni  6359  tz7.44lem1  6418  tz7.44-3  6421  en1b  6929  disjen  7018  domss2  7020  fival  7166  fipwuni  7179  supexd  7204  cantnflem1  7391  dfac8clem  7659  onssnum  7667  dfac12lem1  7769  dfac12lem2  7770  fin1a2lem12  8037  hsmexlem1  8052  axdc2lem  8074  ttukeylem3  8138  wrdexb  11449  restid  13338  prdsbas  13357  prdsplusg  13358  prdsmulr  13359  prdsvsca  13360  prdshom  13366  sscpwex  13692  frgpcyg  16527  eltopspOLD  16656  istpsOLD  16658  istopon  16663  tgval  16693  eltg  16695  eltg2  16696  tgss2  16725  ntrval  16773  neiss2  16838  restin  16897  restntr  16912  cnpresti  17016  cnprest  17017  cnprest2  17018  lmcnp  17032  pnrmopn  17071  cnrmnrm  17089  cmpsublem  17126  cmpsub  17127  cmpcld  17129  hausmapdom  17226  txbasex  17261  dfac14lem  17311  uptx  17319  xkopt  17349  xkopjcn  17350  qtopval2  17387  elqtop  17388  fbssfi  17532  ptcmplem2  17747  isppw  20352  hasheuni  23453  insiga  23498  sigagenval  23501  isrrvv  23646  rrvmulc  23655  kur14  23747  cvmscld  23804  relexp0  24025  relexpsucr  24026  nobndlem1  24346  fobigcup  24440  hfuni  24814  fldrels  25113  mnlelt2  25266  intfmu2  25519  qusp  25542  istopxc  25548  islimrs  25580  islimrs3  25581  islimrs4  25582  bwt2  25592  isfne  26268  isfne4b  26270  isref  26279  locfindis  26305  topjoin  26314  fnemeet1  26315  tailfval  26321  supex2g  26419  kelac2  27163  en1uniel  27380  pmtrfv  27395  cnfex  27699  stoweidlem50  27799  stoweidlem57  27806  stoweidlem59  27808  stoweidlem60  27809  bnj1489  29086
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-un 4512
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-v 2790  df-uni 3828
  Copyright terms: Public domain W3C validator