Theorem uniexg 6588

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 4206	. . 3 |- ( x = A -> U. x = U. A )
2	1	eleq1d 2513	. 2 |- ( x = A -> ( U. x e. _V <-> U. A e. _V ) )
3		vex 3048	. . 3 |- x e. _V
4	3	uniex 6587	. 2 |- U. x e. _V
5	2, 4	vtoclg 3107	1 |- ( A e. V -> U. A e. _V )

Syntax hints:   -> wi 4   = wceq 1444   e. wcel 1887   _Vcvv 3045   U.cuni 4198

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-un 6583

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-rex 2743  df-v 3047  df-uni 4199

This theorem is referenced by:  snnex  6597  uniexb  6601  ssonuni  6613  ssonprc  6619  dmexg  6724  rnexg  6725  iunexg  6769  undefval  7023  onovuni  7061  tz7.44lem1  7123  tz7.44-3  7126  en1b  7637  en1uniel  7641  disjen  7729  domss2  7731  fival  7926  fipwuni  7940  supexd  7967  cantnflem1  8194  dfac8clem  8463  onssnum  8471  dfac12lem1  8573  dfac12lem2  8574  fin1a2lem12  8841  hsmexlem1  8856  axdc2lem  8878  ttukeylem3  8941  wrdexb  12683  restid  15332  prdsbas  15355  prdsplusg  15356  prdsmulr  15357  prdsvsca  15358  prdshom  15365  sscpwex  15720  pmtrfv  17093  frgpcyg  19144  istopon  19940  tgval  19970  eltg  19972  eltg2  19973  tgss2  20003  ntrval  20051  neiptoptop  20147  neiptopnei  20148  restin  20182  neitr  20196  restntr  20198  cnpresti  20304  cnprest  20305  cnprest2  20306  lmcnp  20320  pnrmopn  20359  cnrmnrm  20377  cmpsublem  20414  cmpsub  20415  cmpcld  20417  hausmapdom  20515  isref  20524  locfindis  20545  txbasex  20581  dfac14lem  20632  uptx  20640  xkopt  20670  xkopjcn  20671  qtopval2  20711  elqtop  20712  fbssfi  20852  ptcmplem2  21068  cnextfval  21077  cnextcn  21082  tuslem  21282  isppw  24041  elpwunicl  28168  acunirnmpt2  28262  acunirnmpt2f  28263  hasheuni  28906  insiga  28959  sigagenval  28962  braew  29065  omsval  29117  omsvalOLD  29121  omssubaddlem  29127  omssubadd  29128  omssubaddlemOLD  29131  omssubaddOLD  29132  omsmeas  29155  omsmeasOLD  29156  sibfof  29173  sitmcl  29184  isrrvv  29276  rrvmulc  29286  bnj1489  29865  kur14  29939  cvmscld  29996  nobndlem1  30581  fobigcup  30667  hfuni  30951  isfne  30995  isfne4b  30997  topjoin  31021  fnemeet1  31022  tailfval  31028  mbfresfi  31987  supex2g  32064  kelac2  35923  cnfex  37349  unidmex  37388  pwpwuni  37397  stoweidlem50  37911  stoweidlem57  37918  stoweidlem59  37920  stoweidlem60  37921  fourierdlem71  38041  salgenval  38182  intsaluni  38188  intsal  38189  salgenn0  38190  caragenval  38314  omecl  38324  caragenunidm  38329