Theorem uniexg 6607

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 4198	. . 3 |- ( x = A -> U. x = U. A )
2	1	eleq1d 2533	. 2 |- ( x = A -> ( U. x e. _V <-> U. A e. _V ) )
3		vex 3034	. . 3 |- x e. _V
4	3	uniex 6606	. 2 |- U. x e. _V
5	2, 4	vtoclg 3093	1 |- ( A e. V -> U. A e. _V )

Syntax hints:   -> wi 4   = wceq 1452   e. wcel 1904   _Vcvv 3031   U.cuni 4190

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-un 6602

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-rex 2762  df-v 3033  df-uni 4191

This theorem is referenced by:  snnex  6616  uniexb  6620  ssonuni  6632  ssonprc  6638  dmexg  6743  rnexg  6744  iunexg  6788  undefval  7041  onovuni  7079  tz7.44lem1  7141  tz7.44-3  7144  en1b  7655  en1uniel  7659  disjen  7747  domss2  7749  fival  7944  fipwuni  7958  supexd  7985  cantnflem1  8212  dfac8clem  8481  onssnum  8489  dfac12lem1  8591  dfac12lem2  8592  fin1a2lem12  8859  hsmexlem1  8874  axdc2lem  8896  ttukeylem3  8959  wrdexb  12730  restid  15410  prdsbas  15433  prdsplusg  15434  prdsmulr  15435  prdsvsca  15436  prdshom  15443  sscpwex  15798  pmtrfv  17171  frgpcyg  19221  istopon  20017  tgval  20047  eltg  20049  eltg2  20050  tgss2  20080  ntrval  20128  neiptoptop  20224  neiptopnei  20225  restin  20259  neitr  20273  restntr  20275  cnpresti  20381  cnprest  20382  cnprest2  20383  lmcnp  20397  pnrmopn  20436  cnrmnrm  20454  cmpsublem  20491  cmpsub  20492  cmpcld  20494  hausmapdom  20592  isref  20601  locfindis  20622  txbasex  20658  dfac14lem  20709  uptx  20717  xkopt  20747  xkopjcn  20748  qtopval2  20788  elqtop  20789  fbssfi  20930  ptcmplem2  21146  cnextfval  21155  cnextcn  21160  tuslem  21360  isppw  24120  elpwunicl  28246  acunirnmpt2  28337  acunirnmpt2f  28338  hasheuni  28980  insiga  29033  sigagenval  29036  braew  29138  omsval  29190  omsvalOLD  29194  omssubaddlem  29200  omssubadd  29201  omssubaddlemOLD  29204  omssubaddOLD  29205  omsmeas  29228  omsmeasOLD  29229  sibfof  29246  sitmcl  29257  isrrvv  29349  rrvmulc  29359  bnj1489  29937  kur14  30011  cvmscld  30068  nobndlem1  30652  fobigcup  30738  hfuni  31022  isfne  31066  isfne4b  31068  topjoin  31092  fnemeet1  31093  tailfval  31099  mbfresfi  32051  supex2g  32128  kelac2  35994  cnfex  37412  unidmex  37447  pwpwuni  37456  unirnmap  37560  stoweidlem50  38023  stoweidlem57  38030  stoweidlem59  38032  stoweidlem60  38033  fourierdlem71  38153  salgenval  38294  intsaluni  38300  intsal  38301  salgenn0  38302  caragenval  38433  omecl  38443  caragenunidm  38448