Theorem uniexg 6570

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 4243	. . 3 |- ( x = A -> U. x = U. A )
2	1	eleq1d 2523	. 2 |- ( x = A -> ( U. x e. _V <-> U. A e. _V ) )
3		vex 3109	. . 3 |- x e. _V
4	3	uniex 6569	. 2 |- U. x e. _V
5	2, 4	vtoclg 3164	1 |- ( A e. V -> U. A e. _V )

Syntax hints:   -> wi 4   = wceq 1398   e. wcel 1823   _Vcvv 3106   U.cuni 4235

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-un 6565

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rex 2810  df-v 3108  df-uni 4236

This theorem is referenced by:  snnex  6579  uniexb  6583  ssonuni  6595  ssonprc  6600  dmexg  6704  rnexg  6705  iunexg  6749  undefval  6997  onovuni  7005  tz7.44lem1  7063  tz7.44-3  7066  en1b  7576  en1uniel  7580  disjen  7667  domss2  7669  fival  7864  fipwuni  7878  supexd  7904  cantnflem1  8099  cantnflem1OLD  8122  dfac8clem  8404  onssnum  8412  dfac12lem1  8514  dfac12lem2  8515  fin1a2lem12  8782  hsmexlem1  8797  axdc2lem  8819  ttukeylem3  8882  wrdexb  12545  restid  14923  prdsbas  14946  prdsplusg  14947  prdsmulr  14948  prdsvsca  14949  prdshom  14956  sscpwex  15303  pmtrfv  16676  frgpcyg  18785  eltopspOLD  19586  istpsOLD  19588  istopon  19593  tgval  19623  eltg  19625  eltg2  19626  tgss2  19656  ntrval  19704  neiptoptop  19799  neiptopnei  19800  restin  19834  neitr  19848  restntr  19850  cnpresti  19956  cnprest  19957  cnprest2  19958  lmcnp  19972  pnrmopn  20011  cnrmnrm  20029  cmpsublem  20066  cmpsub  20067  cmpcld  20069  hausmapdom  20167  isref  20176  locfindis  20197  txbasex  20233  dfac14lem  20284  uptx  20292  xkopt  20322  xkopjcn  20323  qtopval2  20363  elqtop  20364  fbssfi  20504  ptcmplem2  20719  cnextfval  20728  cnextcn  20733  tuslem  20936  isppw  23586  acunirnmpt2  27727  acunirnmpt2f  27728  hasheuni  28314  insiga  28367  sigagenval  28370  braew  28451  omsval  28501  omssubaddlem  28507  omssubadd  28508  omsmeas  28531  sibfof  28546  isrrvv  28646  rrvmulc  28656  kur14  28924  cvmscld  28982  nobndlem1  29692  fobigcup  29778  hfuni  30069  mbfresfi  30301  isfne  30397  isfne4b  30399  topjoin  30423  fnemeet1  30424  tailfval  30430  supex2g  30468  kelac2  31250  cnfex  31643  stoweidlem50  32071  stoweidlem57  32078  stoweidlem59  32080  stoweidlem60  32081  fourierdlem71  32199  bnj1489  34513