Theorem uniexg 6382

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.

Step	Hyp	Ref	Expression
1		unieq 4104	. . 3 |- ( x = A -> U. x = U. A )
2	1	eleq1d 2509	. 2 |- ( x = A -> ( U. x e. _V <-> U. A e. _V ) )
3		vex 2980	. . 3 |- x e. _V
4	3	uniex 6381	. 2 |- U. x e. _V
5	2, 4	vtoclg 3035	1 |- ( A e. V -> U. A e. _V )

Syntax hints:   -> wi 4   = wceq 1369   e. wcel 1756   _Vcvv 2977   U.cuni 4096

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4418  ax-un 6377

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-rex 2726  df-v 2979  df-uni 4097

This theorem is referenced by:  snnex  6387  uniexb  6391  ssonuni  6403  ssonprc  6408  dmexg  6514  rnexg  6515  iunexg  6558  undefval  6800  onovuni  6808  tz7.44lem1  6866  tz7.44-3  6869  en1b  7382  en1uniel  7386  disjen  7473  domss2  7475  fival  7667  fipwuni  7681  supexd  7708  cantnflem1  7902  cantnflem1OLD  7925  dfac8clem  8207  onssnum  8215  dfac12lem1  8317  dfac12lem2  8318  fin1a2lem12  8585  hsmexlem1  8600  axdc2lem  8622  ttukeylem3  8685  wrdexb  12250  restid  14377  prdsbas  14400  prdsplusg  14401  prdsmulr  14402  prdsvsca  14403  prdshom  14410  sscpwex  14733  pmtrfv  15963  frgpcyg  18011  eltopspOLD  18528  istpsOLD  18530  istopon  18535  tgval  18565  eltg  18567  eltg2  18568  tgss2  18597  ntrval  18645  neiptoptop  18740  neiptopnei  18741  restin  18775  neitr  18789  restntr  18791  cnpresti  18897  cnprest  18898  cnprest2  18899  lmcnp  18913  pnrmopn  18952  cnrmnrm  18970  cmpsublem  19007  cmpsub  19008  cmpcld  19010  bwthOLD  19019  hausmapdom  19109  txbasex  19144  dfac14lem  19195  uptx  19203  xkopt  19233  xkopjcn  19234  qtopval2  19274  elqtop  19275  fbssfi  19415  ptcmplem2  19630  cnextfval  19639  cnextcn  19644  tuslem  19847  isppw  22457  hasheuni  26539  insiga  26585  sigagenval  26588  braew  26663  omsval  26713  sibfof  26731  isrrvv  26831  rrvmulc  26841  kur14  27109  cvmscld  27167  relexp0  27336  relexpsucr  27337  nobndlem1  27838  fobigcup  27936  hfuni  28227  mbfresfi  28443  isfne  28545  isfne4b  28547  isref  28556  locfindis  28582  topjoin  28591  fnemeet1  28592  tailfval  28598  supex2g  28636  kelac2  29423  cnfex  29755  stoweidlem50  29850  stoweidlem57  29857  stoweidlem59  29859  stoweidlem60  29860  bnj1489  32052