Theorem uniexg 6579

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 4253	. . 3 |- ( x = A -> U. x = U. A )
2	1	eleq1d 2536	. 2 |- ( x = A -> ( U. x e. _V <-> U. A e. _V ) )
3		vex 3116	. . 3 |- x e. _V
4	3	uniex 6578	. 2 |- U. x e. _V
5	2, 4	vtoclg 3171	1 |- ( A e. V -> U. A e. _V )

Syntax hints:   -> wi 4   = wceq 1379   e. wcel 1767   _Vcvv 3113   U.cuni 4245

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-un 6574

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rex 2820  df-v 3115  df-uni 4246

This theorem is referenced by:  snnex  6584  uniexb  6588  ssonuni  6600  ssonprc  6605  dmexg  6712  rnexg  6713  iunexg  6757  undefval  7002  onovuni  7010  tz7.44lem1  7068  tz7.44-3  7071  en1b  7580  en1uniel  7584  disjen  7671  domss2  7673  fival  7868  fipwuni  7882  supexd  7909  cantnflem1  8104  cantnflem1OLD  8127  dfac8clem  8409  onssnum  8417  dfac12lem1  8519  dfac12lem2  8520  fin1a2lem12  8787  hsmexlem1  8802  axdc2lem  8824  ttukeylem3  8887  wrdexb  12520  restid  14685  prdsbas  14708  prdsplusg  14709  prdsmulr  14710  prdsvsca  14711  prdshom  14718  sscpwex  15041  pmtrfv  16273  frgpcyg  18379  eltopspOLD  19186  istpsOLD  19188  istopon  19193  tgval  19223  eltg  19225  eltg2  19226  tgss2  19255  ntrval  19303  neiptoptop  19398  neiptopnei  19399  restin  19433  neitr  19447  restntr  19449  cnpresti  19555  cnprest  19556  cnprest2  19557  lmcnp  19571  pnrmopn  19610  cnrmnrm  19628  cmpsublem  19665  cmpsub  19666  cmpcld  19668  bwthOLD  19677  hausmapdom  19767  txbasex  19802  dfac14lem  19853  uptx  19861  xkopt  19891  xkopjcn  19892  qtopval2  19932  elqtop  19933  fbssfi  20073  ptcmplem2  20288  cnextfval  20297  cnextcn  20302  tuslem  20505  isppw  23116  hasheuni  27731  insiga  27777  sigagenval  27780  braew  27854  omsval  27904  sibfof  27922  isrrvv  28022  rrvmulc  28032  kur14  28300  cvmscld  28358  relexp0  28527  relexpsucr  28528  nobndlem1  29029  fobigcup  29127  hfuni  29418  mbfresfi  29638  isfne  29740  isfne4b  29742  isref  29751  locfindis  29777  topjoin  29786  fnemeet1  29787  tailfval  29793  supex2g  29831  kelac2  30615  cnfex  30981  stoweidlem50  31350  stoweidlem57  31357  stoweidlem59  31359  stoweidlem60  31360  fourierdlem71  31478  bnj1489  33191