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

Theorem uniexg 4706
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 4024 . . 3  |-  ( x  =  A  ->  U. x  =  U. A )
21eleq1d 2502 . 2  |-  ( x  =  A  ->  ( U. x  e.  _V  <->  U. A  e.  _V )
)
3 vex 2959 . . 3  |-  x  e. 
_V
43uniex 4705 . 2  |-  U. x  e.  _V
52, 4vtoclg 3011 1  |-  ( A  e.  V  ->  U. A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    e. wcel 1725   _Vcvv 2956   U.cuni 4015
This theorem is referenced by:  snnex  4713  uniexb  4752  ssonuni  4767  ssonprc  4772  dmexg  5130  rnexg  5131  iunexg  5987  undefval  6546  onovuni  6604  tz7.44lem1  6663  tz7.44-3  6666  en1b  7175  disjen  7264  domss2  7266  fival  7417  fipwuni  7431  supexd  7458  cantnflem1  7645  dfac8clem  7913  onssnum  7921  dfac12lem1  8023  dfac12lem2  8024  fin1a2lem12  8291  hsmexlem1  8306  axdc2lem  8328  ttukeylem3  8391  wrdexb  11763  restid  13661  prdsbas  13680  prdsplusg  13681  prdsmulr  13682  prdsvsca  13683  prdshom  13689  sscpwex  14015  frgpcyg  16854  eltopspOLD  16983  istpsOLD  16985  istopon  16990  tgval  17020  eltg  17022  eltg2  17023  tgss2  17052  ntrval  17100  neiptoptop  17195  neiptopnei  17196  restin  17230  neitr  17244  restntr  17246  cnpresti  17352  cnprest  17353  cnprest2  17354  lmcnp  17368  pnrmopn  17407  cnrmnrm  17425  cmpsublem  17462  cmpsub  17463  cmpcld  17465  bwth  17473  hausmapdom  17563  txbasex  17598  dfac14lem  17649  uptx  17657  xkopt  17687  xkopjcn  17688  qtopval2  17728  elqtop  17729  fbssfi  17869  ptcmplem2  18084  cnextfval  18093  cnextcn  18098  tuslem  18297  isppw  20897  hasheuni  24475  insiga  24520  sigagenval  24523  braew  24593  sibfof  24654  sitmcl  24663  isrrvv  24701  rrvmulc  24711  kur14  24902  cvmscld  24960  relexp0  25129  relexpsucr  25130  nobndlem1  25647  fobigcup  25745  hfuni  26125  mbfresfi  26253  isfne  26348  isfne4b  26350  isref  26359  locfindis  26385  topjoin  26394  fnemeet1  26395  tailfval  26401  supex2g  26439  kelac2  27140  en1uniel  27357  pmtrfv  27372  cnfex  27675  stoweidlem50  27775  stoweidlem57  27782  stoweidlem59  27784  stoweidlem60  27785  bnj1489  29425
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-sep 4330  ax-un 4701
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rex 2711  df-v 2958  df-uni 4016
  Copyright terms: Public domain W3C validator