Theorem uniexg 6582

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 4242	. . 3 |- ( x = A -> U. x = U. A )
2	1	eleq1d 2512	. 2 |- ( x = A -> ( U. x e. _V <-> U. A e. _V ) )
3		vex 3098	. . 3 |- x e. _V
4	3	uniex 6581	. 2 |- U. x e. _V
5	2, 4	vtoclg 3153	1 |- ( A e. V -> U. A e. _V )

Syntax hints:   -> wi 4   = wceq 1383   e. wcel 1804   _Vcvv 3095   U.cuni 4234

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-un 6577

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rex 2799  df-v 3097  df-uni 4235

This theorem is referenced by:  snnex  6591  uniexb  6595  ssonuni  6607  ssonprc  6612  dmexg  6716  rnexg  6717  iunexg  6761  undefval  7007  onovuni  7015  tz7.44lem1  7073  tz7.44-3  7076  en1b  7585  en1uniel  7589  disjen  7676  domss2  7678  fival  7874  fipwuni  7888  supexd  7915  cantnflem1  8111  cantnflem1OLD  8134  dfac8clem  8416  onssnum  8424  dfac12lem1  8526  dfac12lem2  8527  fin1a2lem12  8794  hsmexlem1  8809  axdc2lem  8831  ttukeylem3  8894  wrdexb  12537  restid  14708  prdsbas  14731  prdsplusg  14732  prdsmulr  14733  prdsvsca  14734  prdshom  14741  sscpwex  15061  pmtrfv  16351  frgpcyg  18485  eltopspOLD  19292  istpsOLD  19294  istopon  19299  tgval  19329  eltg  19331  eltg2  19332  tgss2  19362  ntrval  19410  neiptoptop  19505  neiptopnei  19506  restin  19540  neitr  19554  restntr  19556  cnpresti  19662  cnprest  19663  cnprest2  19664  lmcnp  19678  pnrmopn  19717  cnrmnrm  19735  cmpsublem  19772  cmpsub  19773  cmpcld  19775  bwthOLD  19784  hausmapdom  19874  isref  19883  locfindis  19904  txbasex  19940  dfac14lem  19991  uptx  19999  xkopt  20029  xkopjcn  20030  qtopval2  20070  elqtop  20071  fbssfi  20211  ptcmplem2  20426  cnextfval  20435  cnextcn  20440  tuslem  20643  isppw  23260  hasheuni  27964  insiga  28010  sigagenval  28013  braew  28087  omsval  28137  sibfof  28155  isrrvv  28255  rrvmulc  28265  kur14  28533  cvmscld  28591  relexp0  28925  relexpsucr  28926  nobndlem1  29427  fobigcup  29525  hfuni  29816  mbfresfi  30036  isfne  30132  isfne4b  30134  topjoin  30158  fnemeet1  30159  tailfval  30165  supex2g  30203  kelac2  30986  cnfex  31357  stoweidlem50  31721  stoweidlem57  31728  stoweidlem59  31730  stoweidlem60  31731  fourierdlem71  31849  bnj1489  33845