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

Theorem uniexg 4533
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 3852 . . 3  |-  ( x  =  A  ->  U. x  =  U. A )
21eleq1d 2362 . 2  |-  ( x  =  A  ->  ( U. x  e.  _V  <->  U. A  e.  _V )
)
3 vex 2804 . . 3  |-  x  e. 
_V
43uniex 4532 . 2  |-  U. x  e.  _V
52, 4vtoclg 2856 1  |-  ( A  e.  V  ->  U. A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    e. wcel 1696   _Vcvv 2801   U.cuni 3843
This theorem is referenced by:  snnex  4540  uniexb  4579  ssonuni  4594  ssonprc  4599  dmexg  4955  rnexg  4956  iunexg  5783  undefval  6317  onovuni  6375  tz7.44lem1  6434  tz7.44-3  6437  en1b  6945  disjen  7034  domss2  7036  fival  7182  fipwuni  7195  supexd  7220  cantnflem1  7407  dfac8clem  7675  onssnum  7683  dfac12lem1  7785  dfac12lem2  7786  fin1a2lem12  8053  hsmexlem1  8068  axdc2lem  8090  ttukeylem3  8154  wrdexb  11465  restid  13354  prdsbas  13373  prdsplusg  13374  prdsmulr  13375  prdsvsca  13376  prdshom  13382  sscpwex  13708  frgpcyg  16543  eltopspOLD  16672  istpsOLD  16674  istopon  16679  tgval  16709  eltg  16711  eltg2  16712  tgss2  16741  ntrval  16789  neiss2  16854  restin  16913  restntr  16928  cnpresti  17032  cnprest  17033  cnprest2  17034  lmcnp  17048  pnrmopn  17087  cnrmnrm  17105  cmpsublem  17142  cmpsub  17143  cmpcld  17145  hausmapdom  17242  txbasex  17277  dfac14lem  17327  uptx  17335  xkopt  17365  xkopjcn  17366  qtopval2  17403  elqtop  17404  fbssfi  17548  ptcmplem2  17763  isppw  20368  hasheuni  23468  insiga  23513  sigagenval  23516  isrrvv  23661  rrvmulc  23670  kur14  23762  cvmscld  23819  relexp0  24040  relexpsucr  24041  nobndlem1  24417  fobigcup  24511  hfuni  24886  fldrels  25216  mnlelt2  25369  intfmu2  25622  qusp  25645  istopxc  25651  islimrs  25683  islimrs3  25684  islimrs4  25685  bwt2  25695  isfne  26371  isfne4b  26373  isref  26382  locfindis  26408  topjoin  26417  fnemeet1  26418  tailfval  26424  supex2g  26522  kelac2  27266  en1uniel  27483  pmtrfv  27498  cnfex  27802  stoweidlem50  27902  stoweidlem57  27909  stoweidlem59  27911  stoweidlem60  27912  bnj1489  29402
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-un 4528
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rex 2562  df-v 2803  df-uni 3844
  Copyright terms: Public domain W3C validator